SpanRank

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

Statistics

Metric	Count
Definitions generators, spanFinrank, spanRank	3
Theorems lift_spanRank_map_eq_of_ringEquiv, lift_spanRank_map_le, spanFinrank_map_eq_of_ringEquiv, spanFinrank_map_le_of_fg, spanRank_map_eq_of_ringEquiv, spanRank_map_le, mk_eq_spanRank, finrank_eq_spanFinrank_of_free, exists_span_set_encard_eq_spanFinrank, finite_generators, generators_mem, generators_ncard, spanRank_eq_iff, spanRank_eq_spanFinrank, spanRank_le_iff, spanRank_le_iff_exists_span_set_card_le, exists_span_set_card_eq_spanRank, fg_iff_spanRank_eq_spanFinrank, generators_card, instNonemptySubtypeSetEqSpan, le_spanRank_restrictScalars, lift_spanRank_le_iff_exists_span_set_card_le, lift_spanRank_map_eq_of_injective, lift_spanRank_map_le, rank_eq_spanRank_of_free, rank_le_spanRank, spanFinrank_bot, spanFinrank_eq_iInf, spanFinrank_eq_zero_iff_eq_bot, spanFinrank_map_eq_of_injective, spanFinrank_map_le_of_fg, spanFinrank_of_not_fg, spanFinrank_singleton, spanFinrank_span_le_encard, spanFinrank_span_le_ncard_of_finite, spanFinrank_top, spanRank_bot, spanRank_eq_of_equiv, spanRank_eq_zero_iff_eq_bot, spanRank_finite_iff_fg, spanRank_map_eq_of_injective, spanRank_map_le, spanRank_range_le, spanRank_restrictScalars_eq, spanRank_span_le_card, spanRank_span_of_linearIndepOn, spanRank_span_range_of_linearIndependent, spanRank_sup_le_sum_spanRank, spanRank_toENat_eq_iInf_encard, spanRank_toENat_eq_iInf_finset_card, spanRank_top, span_generators	52
Total	55

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lift_spanRank_map_eq_of_ringEquiv 📖	mathematical	—	Cardinal.lift Submodule.spanRank NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule map RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike	—	LE.le.antisymm RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass lift_spanRank_map_le map_of_equiv
lift_spanRank_map_le 📖	mathematical	—	Cardinal Cardinal.instLE Cardinal.lift Submodule.spanRank NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule map RingHom RingHom.instFunLike	—	Submodule.generators_card Submodule.lift_spanRank_le_iff_exists_span_set_card_le Cardinal.mk_image_le_lift le_antisymm span_le mem_map_of_mem subset_span Submodule.span_generators map_le_of_le_comap RingHom.instRingHomClass map_span submodule_span_eq
spanFinrank_map_eq_of_ringEquiv 📖	mathematical	—	Submodule.spanFinrank NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule map RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike	—	Submodule.spanFinrank.eq_1 Cardinal.toNat_lift lift_spanRank_map_eq_of_ringEquiv
spanFinrank_map_le_of_fg 📖	mathematical	FG	Submodule.spanFinrank NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule map RingHom RingHom.instFunLike	—	Submodule.FG.spanRank_le_iff FG.map Cardinal.lift_le Cardinal.lift_natCast Submodule.FG.spanRank_eq_spanFinrank lift_spanRank_map_le
spanRank_map_eq_of_ringEquiv 📖	mathematical	—	Submodule.spanRank NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule map RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike	—	Cardinal.lift_id lift_spanRank_map_eq_of_ringEquiv
spanRank_map_le 📖	mathematical	—	Cardinal Cardinal.instLE Submodule.spanRank NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule map RingHom RingHom.instFunLike	—	Cardinal.lift_id lift_spanRank_map_le

Module

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finrank_eq_spanFinrank_of_free 📖	mathematical	—	finrank Submodule.spanFinrank Top.top Submodule Submodule.instTop	—	Submodule.rank_eq_spanRank_of_free

Module.Basis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk_eq_spanRank 📖	mathematical	—	Set.Elem Set.range DFunLike.coe Module.Basis instFunLike Submodule.spanRank Top.top Submodule Submodule.instTop	—	span_eq Submodule.spanRank_span_of_linearIndepOn LinearIndependent.linearIndepOn_id linearIndependent

Submodule

Definitions

Name	Category	Theorems
generators 📖	CompOp	5 math math: generators_card, FG.generators_ncard, FG.finite_generators, FG.generators_mem, span_generators
spanFinrank 📖	CompOp	36 math math: fg_iff_spanRank_eq_spanFinrank, Ideal.height_le_spanFinrank, PowerSeries.spanFinrank_le_spanFinrank_map_constantCoeff_add_one_of_X_mem, spanFinrank_span_le_ncard_of_finite, PowerSeries.spanFinrank_le_spanFinrank_map_constantCoeff_add_one_of_isPrime, FG.spanRank_eq_spanFinrank, IsLocalRing.spanFinrank_maximalIdeal_eq_finrank_cotangentSpace_of_fg, spanFinrank_map_eq_of_injective, spanFinrank_span_le_encard, ringKrullDim_le_spanFinrank_maximalIdeal, ringKrullDim_le_ringKrullDim_quotient_add_spanFinrank, Ideal.spanFinrank_map_le_of_fg, PowerSeries.spanFinrank_eq_spanFinrank_map_constantCoeff_of_X_notMem_of_fg_of_isPrime, IsRegularLocalRing.spanFinrank_maximalIdeal, TensorProduct.spanFinrank_top_le_of_fg, isRegularLocalRing_iff, spanFinrank_singleton, TensorProduct.spanFinrank_top_eq_of_residueField, Module.finrank_eq_spanFinrank_of_free, FG.spanRank_eq_iff, spanFinrank_top, FG.spanFinrank_baseChange_le, FG.generators_ncard, height_le_ringKrullDim_quotient_add_spanFinrank, FG.spanRank_le_iff, spanFinrank_eq_zero_iff_eq_bot, spanFinrank_bot, ringKrullDim_le_ringKrullDim_add_spanFinrank, spanFinrank_of_not_fg, IsLocalRing.spanFinrank_maximalIdeal_eq_finrank_cotangentSpace, Ideal.height_le_height_add_spanFinrank_of_le, spanFinrank_map_le_of_fg, FG.exists_span_set_encard_eq_spanFinrank, Ideal.spanFinrank_map_eq_of_ringEquiv, IsLocalRing.spanFinrank_eq_finrank_quotient, spanFinrank_eq_iInf
spanRank 📖	CompOp	41 math math: fg_iff_spanRank_eq_spanFinrank, Ideal.height_le_spanRank, Ideal.height_le_iff_exists_minimalPrimes, generators_card, spanRank_map_le, exists_spanRank_le_and_le_height_of_le_height, spanRank_toENat_eq_iInf_encard, FG.spanRank_eq_spanFinrank, rank_le_spanRank, Ideal.spanRank_map_eq_of_ringEquiv, Ideal.lift_spanRank_map_eq_of_ringEquiv, spanRank_range_le, spanRank_span_of_linearIndepOn, spanRank_span_le_card, lift_spanRank_map_le, le_spanRank_restrictScalars, exists_span_set_card_eq_spanRank, spanRank_finite_iff_fg, Ideal.height_le_spanRank_toENat_of_mem_minimal_primes, spanRank_restrictScalars_eq, spanRank_baseChange_le, Ideal.spanRank_map_le, rank_eq_spanRank_of_free, spanRank_map_eq_of_injective, spanRank_toENat_eq_iInf_finset_card, spanRank_sup_le_sum_spanRank, spanRank_span_range_of_linearIndependent, FG.spanRank_eq_iff, FG.spanRank_le_iff, spanRank_eq_zero_iff_eq_bot, spanRank_top, Ideal.exists_spanRank_eq_and_height_eq, lift_spanRank_map_eq_of_injective, Ideal.height_le_spanRank_toENat, Module.Basis.mk_eq_spanRank, spanRank_eq_of_equiv, Ideal.lift_spanRank_map_le, FG.spanRank_le_iff_exists_span_set_card_le, lift_spanRank_le_iff_exists_span_set_card_le, TensorProduct.spanRank_top_le, spanRank_bot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_span_set_card_eq_spanRank 📖	mathematical	—	Set Set.Elem spanRank span	—	spanRank.eq_1 csInf_mem Cardinal.instWellFoundedLT IsScalarTower.left span_coe_eq_restrictScalars restrictScalars_self
fg_iff_spanRank_eq_spanFinrank 📖	mathematical	—	spanRank Cardinal Cardinal.instNatCast spanFinrank FG	—	spanFinrank.eq_1 spanRank_finite_iff_fg Cardinal.cast_toNat_eq_iff_lt_aleph0
generators_card 📖	mathematical	—	Set.Elem generators spanRank	—	exists_span_set_card_eq_spanRank
instNonemptySubtypeSetEqSpan 📖	mathematical	—	Set Submodule span	—	IsScalarTower.left span_coe_eq_restrictScalars restrictScalars_self
le_spanRank_restrictScalars 📖	mathematical	—	Cardinal Cardinal.instLE spanRank CommSemiring.toSemiring restrictScalars Algebra.toSMul	—	exists_span_set_card_eq_spanRank le_imp_le_of_le_of_le spanRank_span_le_card le_refl le_antisymm span_le Eq.le LE.le.trans Eq.ge span_le_restrictScalars
lift_spanRank_le_iff_exists_span_set_card_le 📖	mathematical	—	Cardinal Cardinal.instLE Cardinal.lift spanRank Set Set.Elem span	—	exists_span_set_card_eq_spanRank LE.le.trans Cardinal.lift_le spanRank_span_le_card
lift_spanRank_map_eq_of_injective 📖	mathematical	DFunLike.coe LinearMap LinearMap.instFunLike	Cardinal.lift spanRank map	—	LE.le.antisymm lift_spanRank_map_le exists_span_set_card_eq_spanRank Set.subset_range_iff_exists_image_eq HasSubset.Subset.trans Set.instIsTransSubset subset_span Eq.le LinearMap.map_le_range Cardinal.mk_image_eq_lift Cardinal.lift_le le_imp_le_of_le_of_le spanRank_span_le_card le_refl span_image map_injective_of_injective
lift_spanRank_map_le 📖	mathematical	—	Cardinal Cardinal.instLE Cardinal.lift spanRank map	—	generators_card lift_spanRank_le_iff_exists_span_set_card_le Cardinal.mk_image_le_lift le_antisymm span_le subset_span span_generators span_image map.congr_simp instReflLe
rank_eq_spanRank_of_free 📖	mathematical	—	Module.rank spanRank Top.top Submodule instTop	—	Module.Basis.mk_eq_rank'' Module.Basis.mk_eq_spanRank rankCondition_of_strongRankCondition Cardinal.lift_id Cardinal.mk_range_eq_of_injective Module.Basis.injective nontrivial_of_invariantBasisNumber invariantBasisNumber_of_rankCondition
rank_le_spanRank 📖	mathematical	—	Cardinal Cardinal.instLE Module.rank spanRank Top.top Submodule instTop	—	Module.rank_def spanRank.eq_1 ciSup_le' le_ciInf instNonemptySubtypeSetEqSpan linearIndependent_le_span''
spanFinrank_bot 📖	mathematical	—	spanFinrank Bot.bot Submodule instBot	—	—
spanFinrank_eq_iInf 📖	mathematical	—	spanFinrank iInf Finset Submodule span SetLike.coe Finset.instSetLike Nat.instInfSet Finset.card	—	spanRank_toENat_eq_iInf_finset_card ENat.iInf_toNat
spanFinrank_eq_zero_iff_eq_bot 📖	mathematical	FG	spanFinrank Bot.bot Submodule instBot	—	span_generators Set.ncard_eq_zero FG.finite_generators FG.generators_ncard span_empty spanFinrank_bot
spanFinrank_map_eq_of_injective 📖	mathematical	DFunLike.coe LinearMap LinearMap.instFunLike	spanFinrank map	—	spanFinrank.eq_1 Cardinal.toNat_lift lift_spanRank_map_eq_of_injective
spanFinrank_map_le_of_fg 📖	mathematical	FG	spanFinrank map	—	FG.spanRank_le_iff FG.map Cardinal.lift_le Cardinal.lift_natCast FG.spanRank_eq_spanFinrank lift_spanRank_map_le
spanFinrank_of_not_fg 📖	mathematical	FG	spanFinrank	—	Cardinal.toNat_eq_zero spanRank_finite_iff_fg
spanFinrank_singleton 📖	mathematical	—	spanFinrank span Set Set.instSingletonSet	—	le_antisymm le_trans spanFinrank_span_le_ncard_of_finite Set.ncard_singleton instReflLe Nat.instNoMaxOrder Nat.instCanonicallyOrderedAdd spanFinrank_eq_zero_iff_eq_bot fg_span_singleton
spanFinrank_span_le_encard 📖	mathematical	—	ENat instLEENat ENat.instNatCast spanFinrank span Set.encard	—	spanFinrank.eq_1 Set.encard.eq_1 ENat.card.eq_1 le_trans MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass OrderRingHom.instRingHomClass OrderRingHom.toRingHom_eq_coe OrderRingHom.monotone' spanRank_span_le_card
spanFinrank_span_le_ncard_of_finite 📖	mathematical	—	spanFinrank span Set.ncard	—	Nat.cast_le IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid le_trans spanFinrank_span_le_encard Eq.ge Set.Finite.cast_ncard_eq
spanFinrank_top 📖	mathematical	—	spanFinrank Submodule SetLike.instMembership setLike addCommMonoid module Top.top instTop	—	spanRank_top
spanRank_bot 📖	mathematical	—	spanRank NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Bot.bot Ideal instBot Cardinal Cardinal.instZero	—	spanRank_eq_zero_iff_eq_bot
spanRank_eq_of_equiv 📖	mathematical	—	spanRank Top.top Submodule instTop	—	RingHomSurjective.invPair spanRank_map_eq_of_injective LinearEquiv.injective map_top LinearEquiv.range
spanRank_eq_zero_iff_eq_bot 📖	mathematical	—	spanRank Cardinal Cardinal.instZero Bot.bot Submodule instBot	—	FG.spanRank_le_iff_exists_span_set_card_le le_refl Cardinal.canonicallyOrderedAdd span_empty spanRank.eq_1 Cardinal.iInf_eq_zero_iff Cardinal.mk_eq_zero Set.instIsEmptyElemEmptyCollection
spanRank_finite_iff_fg 📖	mathematical	—	Cardinal Preorder.toLT PartialOrder.toPreorder Cardinal.partialOrder spanRank Cardinal.aleph0 FG	—	spanRank.eq_1 fg_def csInf_mem Cardinal.instWellFoundedLT IsScalarTower.left span_coe_eq_restrictScalars restrictScalars_self LE.le.trans_lt ciInf_le'
spanRank_map_eq_of_injective 📖	mathematical	DFunLike.coe LinearMap LinearMap.instFunLike	spanRank map	—	Cardinal.lift_id lift_spanRank_map_eq_of_injective
spanRank_map_le 📖	mathematical	—	Cardinal Cardinal.instLE spanRank map	—	Cardinal.lift_id lift_spanRank_map_le
spanRank_range_le 📖	mathematical	—	Cardinal Cardinal.instLE spanRank LinearMap.range Top.top Submodule instTop	—	map_top spanRank_map_le
spanRank_restrictScalars_eq 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	spanRank CommSemiring.toSemiring restrictScalars Algebra.toSMul	—	LE.le.antisymm' le_spanRank_restrictScalars exists_span_set_card_eq_spanRank restrictScalars_span le_imp_le_of_le_of_le spanRank_span_le_card le_refl
spanRank_span_le_card 📖	mathematical	—	Cardinal Cardinal.instLE spanRank span Set.Elem	—	spanRank.eq_1 ciInf_le'
spanRank_span_of_linearIndepOn 📖	mathematical	LinearIndepOn	spanRank span Set.Elem	—	spanRank_span_range_of_linearIndependent Subtype.val_injective Subtype.range_coe_subtype
spanRank_span_range_of_linearIndependent 📖	mathematical	LinearIndependent	spanRank span Set.range	—	le_antisymm le_trans spanRank_span_le_card Cardinal.mk_range_le le_ciInf instNonemptySubtypeSetEqSpan Cardinal.mk_preimage_of_injective_of_subset_range Subtype.val_injective Subtype.range_coe_subtype Cardinal.mk_range_eq Function.Injective.of_comp subset_span Set.mem_range_self Module.Basis.span_apply le_refl Module.Basis.le_span map_injective_of_injective RingHomSurjective.ids injective_subtype map_span Set.image_congr Set.image_preimage_eq_inter_range Set.inter_eq_self_of_subset_left map_top range_subtype
spanRank_sup_le_sum_spanRank 📖	mathematical	—	Cardinal Cardinal.instLE spanRank Submodule SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice completeLattice Cardinal.instAdd	—	FG.spanRank_le_iff_exists_span_set_card_le exists_span_set_card_eq_spanRank Cardinal.mk_union_le span_union
spanRank_toENat_eq_iInf_encard 📖	mathematical	—	DFunLike.coe OrderRingHom Cardinal ENat Semiring.toNonAssocSemiring CommSemiring.toSemiring Cardinal.commSemiring PartialOrder.toPreorder Cardinal.partialOrder instCommSemiringENat instPreorderENat OrderRingHom.instFunLike Cardinal.toENat spanRank iInf Set ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat Submodule span Set.encard	—	spanRank.eq_1 le_antisymm le_iInf₂ Set.encard.eq_1 ENat.card.eq_1 OrderRingHom.monotone' ciInf_le' Cardinal.toENat_comp_ofENat le_ciInf instNonemptySubtypeSetEqSpan le_trans Cardinal.ofENat_toENat_le
spanRank_toENat_eq_iInf_finset_card 📖	mathematical	—	DFunLike.coe OrderRingHom Cardinal ENat Semiring.toNonAssocSemiring CommSemiring.toSemiring Cardinal.commSemiring PartialOrder.toPreorder Cardinal.partialOrder instCommSemiringENat instPreorderENat OrderRingHom.instFunLike Cardinal.toENat spanRank iInf Finset Submodule span SetLike.coe Finset.instSetLike ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat ENat.instNatCast Finset.card	—	spanRank_toENat_eq_iInf_encard eq_or_ne Set.encard_ne_top_iff Finset.finite_toSet le_antisymm le_iInf iInf₂_le iInf_le_of_le Set.Finite.coe_toFinset instReflLe Set.Infinite.encard_eq OrderTop.le_top
spanRank_top 📖	mathematical	—	spanRank Submodule SetLike.instMembership setLike addCommMonoid module Top.top instTop	—	RingHomSurjective.ids map_top range_subtype spanRank_map_eq_of_injective subtype_injective
span_generators 📖	mathematical	—	span generators	—	exists_span_set_card_eq_spanRank

Submodule.FG

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_span_set_encard_eq_spanFinrank 📖	mathematical	Submodule.FG	Set Set.encard ENat ENat.instNatCast Submodule.spanFinrank Submodule.span	—	Submodule.exists_span_set_card_eq_spanRank Submodule.fg_iff_spanRank_eq_spanFinrank Set.encard.eq_1 ENat.card.eq_1 Submodule.spanFinrank.eq_1 map_natCast OrderRingHom.instRingHomClass Cardinal.toNat_natCast
finite_generators 📖	mathematical	Submodule.FG	Set.Finite Submodule.generators	—	Cardinal.lt_aleph0_iff_set_finite Submodule.generators_card Submodule.spanRank_finite_iff_fg
generators_mem 📖	mathematical	—	Set Set.instHasSubset Submodule.generators SetLike.coe Submodule Submodule.setLike	—	Submodule.span_generators Submodule.subset_span
generators_ncard 📖	mathematical	Submodule.FG	Set.ncard Submodule.generators Submodule.spanFinrank	—	Cardinal.instCharZero Submodule.fg_iff_spanRank_eq_spanFinrank Set.ncard.eq_1 Set.encard.eq_1 ENat.card.eq_1 Submodule.generators_card Cardinal.toNat_toENat Submodule.spanFinrank.eq_1
spanRank_eq_iff 📖	mathematical	Submodule.FG	Submodule.spanRank Cardinal Cardinal.instNatCast Submodule.spanFinrank	—	Cardinal.toNat_eq_iff_of_lt_aleph0
spanRank_eq_spanFinrank 📖	mathematical	Submodule.FG	Submodule.spanRank Cardinal Cardinal.instNatCast Submodule.spanFinrank	—	Submodule.fg_iff_spanRank_eq_spanFinrank
spanRank_le_iff 📖	mathematical	Submodule.FG	Cardinal Cardinal.instLE Submodule.spanRank Cardinal.instNatCast Submodule.spanFinrank	—	Cardinal.toNat_le_iff_of_lt_aleph0
spanRank_le_iff_exists_span_set_card_le 📖	mathematical	—	Cardinal Cardinal.instLE Submodule.spanRank Set Set.Elem Submodule.span	—	Cardinal.lift_id Submodule.lift_spanRank_le_iff_exists_span_set_card_le

---

← Back to Index