SpanRankOperations

📁 Source: Mathlib/Algebra/Module/SpanRankOperations.lean

Statistics

Metric	Count
Definitions	0
Theorems spanFinrank_eq_finrank_quotient, spanFinrank_maximalIdeal_eq_finrank_cotangentSpace, spanFinrank_maximalIdeal_eq_finrank_cotangentSpace_of_fg, spanFinrank_baseChange_le, spanRank_baseChange_le, spanFinrank_top_eq_of_residueField, spanFinrank_top_le_of_fg, spanRank_top_le	8
Total	8

IsLocalRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
spanFinrank_eq_finrank_quotient 📖	mathematical	Submodule.FG CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	Submodule.spanFinrank CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Module.finrank HasQuotient.Quotient Ideal Ideal.instHasQuotient_1 maximalIdeal Submodule SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module Submodule.hasQuotient CommRing.toRing Submodule.addCommGroup Submodule.instSMul Semiring.toModule Submodule.isScalarTower' SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribSMul.toSMulZeroClass instDistribSMul NonAssocSemiring.toNonUnitalNonAssocSemiring AddCommMonoid.toAddMonoid DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid IsScalarTower.left DistribMulAction.toMulAction Top.top Submodule.instTop Ideal.Quotient.semiring Submodule.Quotient.addCommGroup Module.instQuotientIdealSubmoduleHSMulTop Ideal.instIsTwoSided_1	—	Submodule.isScalarTower' IsScalarTower.left Ideal.instIsTwoSided_1 Algebra.to_smulCommClass TensorProduct.spanFinrank_top_eq_of_residueField Module.finrank_eq_spanFinrank_of_free commRing_strongRankCondition toNontrivial Field.instIsLocalRing Module.Free.of_divisionRing RingHomInvPair.ids TensorProduct.isScalarTower_left IsScalarTower.right residue_surjective LinearEquiv.finrank_eq
spanFinrank_maximalIdeal_eq_finrank_cotangentSpace 📖	mathematical	—	Submodule.spanFinrank CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule maximalIdeal Module.finrank ResidueField CotangentSpace DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield ResidueField.field AddCommGroup.toAddCommMonoid Ideal.instAddCommGroupCotangent instModuleResidueFieldCotangentSpace	—	spanFinrank_maximalIdeal_eq_finrank_cotangentSpace_of_fg Ideal.fg_of_isNoetherianRing
spanFinrank_maximalIdeal_eq_finrank_cotangentSpace_of_fg 📖	mathematical	Ideal.FG CommSemiring.toSemiring CommRing.toCommSemiring maximalIdeal	Submodule.spanFinrank CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule maximalIdeal Module.finrank ResidueField CotangentSpace DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield ResidueField.field AddCommGroup.toAddCommMonoid Ideal.instAddCommGroupCotangent instModuleResidueFieldCotangentSpace	—	spanFinrank_eq_finrank_quotient

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
spanRank_baseChange_le 📖	mathematical	—	Cardinal Cardinal.instLE spanRank TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring AddCommGroup.toAddCommMonoid Algebra.toModule TensorProduct.addCommMonoid TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass baseChange Cardinal.lift	—	Algebra.to_smulCommClass exists_span_set_card_eq_spanRank TensorProduct.smulCommClass_left smulCommClass_self baseChange_span le_imp_le_of_le_of_le spanRank_span_le_card le_refl Cardinal.lift_id' Cardinal.lift_umax Cardinal.mk_image_le_lift

Submodule.FG

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
spanFinrank_baseChange_le 📖	mathematical	Submodule.FG CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	Submodule.spanFinrank TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring AddCommGroup.toAddCommMonoid Algebra.toModule TensorProduct.addCommMonoid TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass Submodule.baseChange	—	Algebra.to_smulCommClass Submodule.spanFinrank.eq_1 le_imp_le_of_le_of_le Cardinal.toNat_le_toNat Submodule.spanRank_baseChange_le Submodule.spanRank_finite_iff_fg le_refl Cardinal.toNat_lift

TensorProduct

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
spanFinrank_top_eq_of_residueField 📖	mathematical	Submodule.FG CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	Submodule.spanFinrank IsLocalRing.ResidueField TensorProduct CommRing.toCommSemiring Submodule CommSemiring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing IsLocalRing.instCommRingResidueField Submodule.addCommMonoid IsLocalRing.instModuleResidueFieldOfAlgebra Algebra.id Submodule.module DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield IsLocalRing.ResidueField.field addCommMonoid leftModule Semiring.toModule Algebra.to_smulCommClass IsLocalRing.ResidueField.algebra Top.top Submodule.instTop	—	Module.Finite.iff_fg LE.le.antisymm Algebra.to_smulCommClass spanFinrank_top_le_of_fg Submodule.exists_span_set_card_eq_spanRank Cardinal.mk_lt_aleph0_iff Module.Finite.fg_top Module.Finite.base_change smulCommClass_left smulCommClass_self mk_surjective IsLocalRing.residue_surjective Set.image_comp Function.comp_surjInv Set.image_id RingHomSurjective.ids IsLocalRing.map_tensorProduct_mk_eq_top Submodule.map_span isScalarTower_left IsScalarTower.right Submodule.restrictScalars_span Submodule.restrictScalars_eq_top_iff Submodule.spanFinrank_top le_imp_le_of_le_of_le Submodule.spanFinrank_span_le_ncard_of_finite Set.Finite.image le_refl Submodule.spanFinrank.eq_1 Set.ncard_image_le
spanFinrank_top_le_of_fg 📖	mathematical	Submodule.FG CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	Submodule.spanFinrank TensorProduct CommRing.toCommSemiring Submodule CommSemiring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Submodule.addCommMonoid Algebra.toModule Submodule.module addCommMonoid leftModule Semiring.toModule Algebra.to_smulCommClass Top.top Submodule.instTop	—	Algebra.to_smulCommClass Submodule.baseChange_top Submodule.spanFinrank_top le_imp_le_of_le_of_le Submodule.FG.spanFinrank_baseChange_le Submodule.fg_top le_refl
spanRank_top_le 📖	mathematical	—	Cardinal Cardinal.instLE Submodule.spanRank TensorProduct CommRing.toCommSemiring Submodule CommSemiring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Submodule.addCommMonoid Algebra.toModule Submodule.module addCommMonoid leftModule Semiring.toModule Algebra.to_smulCommClass Top.top Submodule.instTop Cardinal.lift	—	Algebra.to_smulCommClass Submodule.baseChange_top Submodule.spanRank_top le_imp_le_of_le_of_le Submodule.spanRank_baseChange_le le_refl

---

← Back to Index