Domain

📁 Source: Mathlib/RingTheory/Flat/Domain.lean

Statistics

Metric	Count
Definitions	0
Theorems tmul_of_isDomain, tmul_of_isDomain, map_injective_of_flat_flat_of_isDomain	3
Total	3

LinearIndepOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tmul_of_isDomain 📖	mathematical	LinearIndepOn CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	TensorProduct TensorProduct.tmul TensorProduct.addCommMonoid TensorProduct.instModule SProd.sprod Set Set.instSProd	—	LinearIndependent.comp LinearIndependent.tmul_of_isDomain Equiv.injective

LinearIndependent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tmul_of_isDomain 📖	mathematical	LinearIndependent CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	TensorProduct TensorProduct.tmul TensorProduct.addCommMonoid TensorProduct.instModule	—	eq_1 RingHomInvPair.ids LinearEquiv.coe_toLinearMap RingHomCompTriple.ids LinearMap.coe_comp Finsupp.lhom_ext' LinearMap.ext_ring Finsupp.linearCombination_single one_smul finsuppTensorFinsupp'_symm_single_eq_single_one_tmul TensorProduct.map_injective_of_flat_flat_of_isDomain Module.Flat.finsupp LinearEquiv.injective

TensorProduct

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_injective_of_flat_flat_of_isDomain 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike	TensorProduct addCommMonoid instModule map	—	Function.Injective.of_comp IsScalarTower.right smulCommClass_left smulCommClass_self Algebra.to_smulCommClass map_injective_of_flat_flat Module.Flat.of_free Module.Free.of_divisionRing IsDomain.toNontrivial IsDomain.to_noZeroDivisors Module.Flat.lTensor_preserves_injective_linearMap Localization.flat Module.Free.self RingHomInvPair.ids IsScalarTower.to_smulCommClass isScalarTower_left LinearEquiv.injective IsScalarTower.left IsScalarTower.to_smulCommClass' OreLocalization.instIsScalarTower Module.Flat.rTensor_preserves_injective_linearMap Module.Flat.instTensorProduct FaithfulSMul.algebraMap_injective FractionRing.instFaithfulSMul Module.Free.instFaithfulSMulOfNontrivial RingHomCompTriple.ids LinearMap.IsScalarTower.compatibleSMul isScalarTower AlgebraTensorModule.curry_injective LinearMap.ext map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass one_smul

---

← Back to Index