Documentation Verification Report

Module

📁 Source: Mathlib/RingTheory/LocalRing/Module.lean

Statistics

Metric	Count
Definitions	0
Theorems `map_mkQ_eq`, `map_mkQ_eq_top`, `map_tensorProduct_mk_eq_top`, `span_eq_top_of_tmul_eq_basis`, `split_injective_iff_lTensor_residueField_injective`, `subsingleton_tensorProduct`, `linearCombination_bijective_of_flat`, `linearIndependent_of_flat`, `exists_basis_of_basis_baseChange`, `exists_basis_of_span_of_flat`, `exists_basis_of_span_of_maximalIdeal_rTensor_injective`, `free_of_flat_of_finrank_eq`, `free_of_flat_of_isLocalRing`, `free_of_lTensor_residueField_injective`, `free_of_maximalIdeal_rTensor_injective`, `mem_support_iff_nontrivial_residueField_tensorProduct`, `nonempty_basis_of_flat_of_finrank_eq`, `lTensor_injective_of_exact_of_exact_of_rTensor_injective`	18
Total	18

IsLocalRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_mkQ_eq` 📖	mathematical	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Submodule.FG`	`Submodule.map` `HasQuotient.Quotient` `Ring.toSemiring` `CommRing.toRing` `Submodule.hasQuotient` `Ideal` `Submodule.instSMul` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `maximalIdeal` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `Submodule.mkQ`	—	`IsScalarTower.left` `RingHomSurjective.ids` `Submodule.comap_map_mkQ` `Submodule.comap_mono` `Eq.ge` `LE.le.antisymm` `Submodule.le_of_le_smul_of_le_jacobson_bot` `jacobson_eq_maximalIdeal` `bot_ne_top` `Ideal.instNontrivial` `toNontrivial` `le_refl` `sup_comm`
`map_mkQ_eq_top` 📖	mathematical	—	`Submodule.map` `HasQuotient.Quotient` `Submodule` `Ring.toSemiring` `CommRing.toRing` `AddCommGroup.toAddCommMonoid` `Submodule.hasQuotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.instSMul` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `maximalIdeal` `Top.top` `Submodule.instTop` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `Submodule.mkQ`	—	`IsScalarTower.left` `RingHomSurjective.ids` `map_mkQ_eq` `le_top` `Module.Finite.fg_top` `Submodule.map_top` `Submodule.range_mkQ`
`map_tensorProduct_mk_eq_top` 📖	mathematical	—	`Submodule.map` `TensorProduct` `CommRing.toCommSemiring` `ResidueField` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRingResidueField` `AddCommGroup.toAddCommMonoid` `Algebra.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `ResidueField.field` `ResidueField.algebra` `Algebra.id` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `DFunLike.coe` `LinearMap` `LinearMap.addCommMonoid` `LinearMap.module` `TensorProduct.smulCommClass_left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `LinearMap.instFunLike` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Top.top` `Submodule` `Submodule.instTop`	—	`RingHomSurjective.ids` `TensorProduct.smulCommClass_left` `smulCommClass_self` `IsScalarTower.left` `IsScalarTower.to_smulCommClass` `instIsScalarTowerResidueField` `IsScalarTower.right` `Submodule.Quotient.isScalarTower` `Submodule.Quotient.smulCommClass` `Ideal.instIsTwoSided_1` `Module.IsTorsionBySet.isScalarTower` `Module.isTorsionBySet_quotient_ideal_smul` `LinearMap.IsScalarTower.compatibleSMul'` `LinearMap.instIsScalarTower` `RingHomInvPair.ids` `LinearMap.instSMulCommClass` `RingHomCompTriple.ids` `LinearMap.ext` `one_smul` `Submodule.mkQ_surjective` `LinearMap.comp_apply` `map_mkQ_eq_top` `LinearMap.range_eq_top` `Submodule.map_top` `Submodule.map_comp` `TensorProduct.mk_surjective` `Ideal.Quotient.mk_surjective`
`span_eq_top_of_tmul_eq_basis` 📖	mathematical	`TensorProduct.tmul` `CommRing.toCommSemiring` `ResidueField` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRingResidueField` `AddCommGroup.toAddCommMonoid` `Algebra.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `ResidueField.field` `ResidueField.algebra` `Algebra.id` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `DFunLike.coe` `Module.Basis` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `Module.Basis.instFunLike`	`Submodule.span` `CommSemiring.toSemiring` `Set.range` `Top.top` `Submodule` `Submodule.instTop`	—	`Algebra.to_smulCommClass` `RingHomSurjective.ids` `TensorProduct.smulCommClass_left` `smulCommClass_self` `map_tensorProduct_mk_eq_top` `Submodule.map_span` `Ideal.instIsTwoSided_1` `TensorProduct.isScalarTower_left` `IsScalarTower.right` `Submodule.restrictScalars_span` `Ideal.Quotient.mk_surjective` `Submodule.restrictScalars_eq_top_iff` `Module.Basis.span_eq` `Set.range_comp`
`split_injective_iff_lTensor_residueField_injective` 📖	mathematical	—	`LinearMap.comp` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `LinearMap.id` `TensorProduct` `ResidueField` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRingResidueField` `Algebra.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `ResidueField.field` `ResidueField.algebra` `Algebra.id` `DFunLike.coe` `LinearMap` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearMap.instFunLike` `LinearMap.lTensor`	—	`RingHomCompTriple.ids` `LinearMap.lTensor_comp` `LinearMap.lTensor_id` `LinearMap.congr_fun` `RingHomSurjective.ids` `Module.free_of_lTensor_residueField_injective` `Submodule.mkQ_surjective` `LinearMap.exact_map_mkQ_range` `List.TFAE.out` `RingHomInvPair.ids` `Function.Exact.split_tfae` `LinearMap.exact_subtype_mkQ` `Subtype.val_injective` `Module.projective_lifting_property` `Module.Projective.of_free` `Module.Projective.of_split` `LinearMap.mem_range_self` `LinearMap.exact_iff` `LinearMap.ker_rangeRestrict` `Submodule.range_subtype` `Module.Finite.of_surjective` `DFunLike.congr_fun` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `LinearMap.comp_apply` `Function.Exact.linearMap_comp_eq_zero` `LinearMap.exact_subtype_ker_map` `LinearMap.lTensor_zero` `LinearMap.zero_apply` `LinearMap.ker_eq_bot` `Submodule.subsingleton_iff_eq_bot` `subsingleton_tensorProduct`
`subsingleton_tensorProduct` 📖	mathematical	—	`TensorProduct` `CommRing.toCommSemiring` `ResidueField` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRingResidueField` `AddCommGroup.toAddCommMonoid` `Algebra.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `ResidueField.field` `ResidueField.algebra` `Algebra.id`	—	`Submodule.subsingleton_iff` `subsingleton_iff_bot_eq_top` `RingHomSurjective.ids` `TensorProduct.smulCommClass_left` `smulCommClass_self` `map_tensorProduct_mk_eq_top` `Submodule.map_bot`

Module

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_basis_of_basis_baseChange` 📖	mathematical	`LinearIndependent` `IsLocalRing.ResidueField` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `IsLocalRing.instCommRingResidueField` `AddCommGroup.toAddCommMonoid` `Algebra.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `IsLocalRing.ResidueField.algebra` `Algebra.id` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearMap.instFunLike` `LinearMap.addCommMonoid` `LinearMap.module` `TensorProduct.smulCommClass_left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `toDistribMulAction` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `Submodule.span` `Set.range` `Top.top` `Submodule` `Submodule.instTop` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `SetLike.instMembership` `Submodule.setLike` `IsLocalRing.maximalIdeal` `Submodule.addCommMonoid` `Submodule.module` `LinearMap.rTensor` `Submodule.subtype`	`Basis` `Basis.instFunLike`	—	`TensorProduct.smulCommClass_left` `smulCommClass_self` `Algebra.to_smulCommClass` `le_refl` `RingHomSurjective.ids` `LinearMap.range_eq_top` `Finsupp.range_linearCombination` `IsLocalRing.span_eq_top_of_tmul_eq_basis` `instFiniteOfFinitePresentation` `Finite.of_fg` `FinitePresentation.fg_ker` `Finite.finsupp` `Finite.finite_basis` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Finite.base_change` `Finite.self` `RingHomInvPair.ids` `LinearMap.ker_eq_bot` `Submodule.subsingleton_iff_eq_bot` `IsLocalRing.subsingleton_tensorProduct` `LinearMap.lTensor_surjective` `Submodule.finrank_eq_zero` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `commRing_strongRankCondition` `FiniteDimensional.finiteDimensional_submodule` `Ideal.instIsTwoSided_1` `LinearMap.finrank_range_add_finrank_ker` `finrank_top` `IsScalarTower.to_smulCommClass` `IsScalarTower.right` `finrank_tensorProduct` `Free.finsupp` `Free.self` `finrank_self` `finrank_finsupp_self` `one_mul` `add_zero` `finrank_eq_card_basis` `lTensor_injective_of_exact_of_exact_of_rTensor_injective` `LinearMap.exact_subtype_mkQ` `Submodule.mkQ_surjective` `LinearMap.exact_subtype_ker_map` `Flat.lTensor_preserves_injective_linearMap` `Flat.of_free` `Subtype.val_injective` `Function.Bijective.injective` `LinearMap.baseChange_eq_ltensor` `RingHomCompTriple.ids` `LinearMap.comp_apply` `LinearMap.lTensor_comp` `Function.Exact.linearMap_comp_eq_zero` `LinearMap.lTensor_zero` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `Finsupp.linearCombination_single` `one_smul`
`exists_basis_of_span_of_flat` 📖	mathematical	`Submodule.span` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Set.range` `Top.top` `Submodule` `Submodule.instTop`	`DFunLike.coe` `Basis` `Basis.instFunLike`	—	`exists_basis_of_span_of_maximalIdeal_rTensor_injective` `Flat.rTensor_preserves_injective_linearMap` `Subtype.val_injective`
`exists_basis_of_span_of_maximalIdeal_rTensor_injective` 📖	mathematical	`TensorProduct` `CommRing.toCommSemiring` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `IsLocalRing.maximalIdeal` `Submodule.addCommMonoid` `AddCommGroup.toAddCommMonoid` `Submodule.module` `DFunLike.coe` `LinearMap` `RingHom.id` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearMap.instFunLike` `LinearMap.rTensor` `Submodule.subtype` `Submodule.span` `Set.range` `Top.top` `Submodule.instTop`	`Basis` `Basis.instFunLike`	—	`RingHomSurjective.ids` `TensorProduct.smulCommClass_left` `smulCommClass_self` `IsLocalRing.map_tensorProduct_mk_eq_top` `instFiniteOfFinitePresentation` `Algebra.to_smulCommClass` `eq_top_iff` `Set.Subset.trans` `Submodule.top_coe` `SetLike.coe_subset_coe` `instIsConcreteLE` `Set.range_comp` `Submodule.span_image` `Submodule.span_subset_span` `TensorProduct.isScalarTower_left` `IsScalarTower.right` `exists_linearIndependent'` `exists_basis_of_basis_baseChange`
`free_of_flat_of_finrank_eq` 📖	mathematical	`finrank` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `MaximalSpectrum.asIdeal` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Ideal.Quotient.commRing` `AddCommGroup.toAddCommMonoid` `Submodule.Quotient.module` `CommRing.toRing` `Ring.toAddCommGroup` `Semiring.toModule` `Ideal.Quotient.semiring` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `Algebra.to_smulCommClass` `Ideal.instAlgebraQuotient` `Algebra.id`	`Free`	—	`Algebra.to_smulCommClass` `nonempty_basis_of_flat_of_finrank_eq` `Free.of_basis`
`free_of_flat_of_isLocalRing` 📖	mathematical	—	`Free` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid`	—	`Algebra.to_smulCommClass` `Free.of_divisionRing` `Ideal.instIsTwoSided_1` `TensorProduct.smulCommClass_left` `smulCommClass_self` `Function.Surjective.comp_left` `TensorProduct.mk_surjective` `Quotient.mk_surjective` `Free.of_basis` `IsLocalRing.linearIndependent_of_flat` `Basis.linearIndependent` `Eq.ge` `IsLocalRing.span_eq_top_of_tmul_eq_basis`
`free_of_lTensor_residueField_injective` 📖	mathematical	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `Function.Exact` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `TensorProduct` `IsLocalRing.ResidueField` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `IsLocalRing.instCommRingResidueField` `Algebra.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `IsLocalRing.ResidueField.algebra` `Algebra.id` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearMap.lTensor`	`Free`	—	`finitePresentation_of_free_of_surjective` `RingHomSurjective.ids` `Function.Exact.linearMap_ker_eq` `LinearMap.range_eq_map` `Submodule.FG.map` `Finite.fg_top` `free_of_maximalIdeal_rTensor_injective` `lTensor_injective_of_exact_of_exact_of_rTensor_injective` `LinearMap.exact_subtype_mkQ` `Submodule.mkQ_surjective` `Flat.lTensor_preserves_injective_linearMap` `Flat.of_free` `Subtype.val_injective`
`free_of_maximalIdeal_rTensor_injective` 📖	mathematical	`TensorProduct` `CommRing.toCommSemiring` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `IsLocalRing.maximalIdeal` `Submodule.addCommMonoid` `AddCommGroup.toAddCommMonoid` `Submodule.module` `DFunLike.coe` `LinearMap` `RingHom.id` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearMap.instFunLike` `LinearMap.rTensor` `Submodule.subtype`	`Free`	—	`exists_basis_of_span_of_maximalIdeal_rTensor_injective` `Set.range_id` `Submodule.span_univ` `Free.of_basis`
`mem_support_iff_nontrivial_residueField_tensorProduct` 📖	mathematical	—	`PrimeSpectrum` `CommRing.toCommSemiring` `Set` `Set.instMembership` `support` `Nontrivial` `TensorProduct` `Ideal.ResidueField` `PrimeSpectrum.asIdeal` `PrimeSpectrum.isPrime` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `IsLocalRing.instCommRingResidueField` `Localization.AtPrime` `OreLocalization.instCommRing` `Ideal.primeCompl` `CommSemiring.toSemiring` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `AddCommGroup.toAddCommMonoid` `Algebra.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `IsLocalRing.ResidueField.algebra` `OreLocalization.instAlgebra` `Algebra.id`	—	`PrimeSpectrum.isPrime` `RingHomInvPair.ids` `Algebra.to_smulCommClass` `IsScalarTower.to_smulCommClass` `IsScalarTower.right` `IsLocalRing.instIsScalarTowerResidueField` `Equiv.nontrivial_congr` `mem_support_iff` `not_iff_not` `not_nontrivial_iff_subsingleton` `IsLocalRing.subsingleton_tensorProduct` `Finite.base_change`
`nonempty_basis_of_flat_of_finrank_eq` 📖	mathematical	`finrank` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `MaximalSpectrum.asIdeal` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Ideal.Quotient.commRing` `AddCommGroup.toAddCommMonoid` `Submodule.Quotient.module` `CommRing.toRing` `Ring.toAddCommGroup` `Semiring.toModule` `Ideal.Quotient.semiring` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `Algebra.to_smulCommClass` `Ideal.instAlgebraQuotient` `Algebra.id`	`Basis`	—	`Algebra.to_smulCommClass` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `MaximalSpectrum.isMaximal` `Field.instIsLocalRing` `Free.of_divisionRing` `Finite.base_change` `TensorProduct.smulCommClass_left` `smulCommClass_self` `RingHomInvPair.ids` `bijective_of_isLocalized_maximal` `Ideal.IsMaximal.isPrime'` `IsScalarTower.right` `instIsLocalizedModuleFinsuppLinearMap` `instIsLocalizedModuleLinearMapOfIsLocalization` `Localization.isLocalization` `IsLocalization.tensorProduct_isLocalizedModule` `LinearMap.CompatibleSMul.finsupp_dom` `LinearMap.IsScalarTower.compatibleSMul'` `TensorProduct.isScalarTower_left` `IsLocalizedModule.map_linearCombination` `LinearMap.coe_restrictScalars` `IsLocalRing.linearCombination_bijective_of_flat` `Localization.AtPrime.isLocalRing` `Flat.instTensorProduct` `Flat.of_free` `Free.self` `IsScalarTower.to_smulCommClass` `IsLocalRing.instIsScalarTowerResidueField` `Equiv.comp_bijective` `instIsScalarTowerQuotientIdealResidueField` `RingHomCompTriple.ids` `IsScalarTower.left` `Finsupp.induction_linear` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `map_add` `SemilinearMapClass.toAddHomClass` `Finsupp.linearCombination_single` `mul_one` `one_smul` `TensorProduct.finsuppScalarRight_symm_apply_single` `Basis.repr_symm_apply` `LinearEquiv.bijective` `Ideal.pi_tensorProductMk_quotient_surjective` `Ideal.isCoprime_of_isMaximal` `Iff.ne` `MaximalSpectrum.ext_iff`

Module.IsLocalRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`linearCombination_bijective_of_flat` 📖	—	`Function.Bijective` `Finsupp` `IsLocalRing.ResidueField` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `IsLocalRing.instCommRingResidueField` `AddCommGroup.toAddCommMonoid` `Algebra.toModule` `IsLocalRing.ResidueField.algebra` `Algebra.id` `DFunLike.coe` `LinearMap` `RingHom.id` `Finsupp.instAddCommMonoid` `TensorProduct.addCommMonoid` `Finsupp.module` `Semiring.toModule` `TensorProduct.leftModule` `Algebra.to_smulCommClass` `LinearMap.instFunLike` `Finsupp.linearCombination` `CommSemiring.toSemiring` `TensorProduct.instModule` `LinearMap.addCommMonoid` `LinearMap.module` `TensorProduct.smulCommClass_left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing`	—	—	`Algebra.to_smulCommClass` `TensorProduct.smulCommClass_left` `smulCommClass_self` `linearIndependent_of_flat` `RingHomSurjective.ids` `LinearMap.range_eq_top` `Finsupp.range_linearCombination` `IsLocalRing.span_eq_top_of_tmul_eq_basis`
`linearIndependent_of_flat` 📖	—	`LinearIndependent` `IsLocalRing.ResidueField` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `IsLocalRing.instCommRingResidueField` `AddCommGroup.toAddCommMonoid` `Algebra.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `IsLocalRing.ResidueField.algebra` `Algebra.id` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearMap.instFunLike` `LinearMap.addCommMonoid` `LinearMap.module` `TensorProduct.smulCommClass_left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass`	—	—	`TensorProduct.smulCommClass_left` `smulCommClass_self` `Algebra.to_smulCommClass` `linearIndependent_iff'` `Finset.induction` `Finset.notMem_empty` `Module.Flat.isTrivialRelation_of_sum_smul_eq_zero` `Finset.sum_coe_sort` `IsScalarTower.left` `LinearIndependent.ne_zero` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Finset.mem_insert_self` `Mathlib.Tactic.Contrapose.contrapose₂` `sum_mem` `Submodule.addSubmonoidClass` `Submodule.smul_mem_smul` `mul_assoc` `IsUnit.val_inv_mul` `mul_one` `eq_neg_iff_add_eq_zero` `Finset.sum_congr` `Finset.sum_insert` `Finset.mem_insert` `Finset.sum_eq_zero` `Ideal.instIsTwoSided_1` `TensorProduct.tmul_add` `TensorProduct.tmul_smul` `TensorProduct.CompatibleSMul.isScalarTower` `IsLocalRing.instIsScalarTowerResidueField` `IsScalarTower.right` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `linearIndependent_add_smul_iff` `neg_zero` `MulZeroClass.zero_mul` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `smul_add` `Finset.sum_add_distrib` `smul_smul` `Finset.sum_smul` `Finset.sum_mul` `mul_neg` `Finset.sum_neg_distrib` `add_comm`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lTensor_injective_of_exact_of_exact_of_rTensor_injective` 📖	—	`Function.Exact` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearMap.rTensor` `LinearMap.lTensor`	—	—	`injective_iff_map_eq_zero` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `LinearMap.rTensor_surjective` `RingHomCompTriple.ids` `LinearMap.comp_apply` `LinearMap.rTensor_comp_lTensor` `LinearMap.lTensor_comp_rTensor` `rTensor_exact` `LinearMap.lTensor_comp` `Function.Exact.linearMap_comp_eq_zero` `LinearMap.lTensor_zero` `map_zero` `AddMonoidHomClass.toZeroHomClass` `lTensor_exact` `LinearMap.rTensor_comp` `LinearMap.rTensor_zero`

---

← Back to Index