SpanRank

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

Statistics

Metric	Count
Definitions `generators`, `spanFinrank`, `spanRank`	3
Theorems `spanFinrank_map_le_of_fg`, `spanRank_map_le`, `mk_eq_spanRank`, `exists_span_set_encard_eq_spanFinrank`, `finite_generators`, `generators_mem`, `generators_ncard`, `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`, `rank_eq_spanRank_of_free`, `rank_le_spanRank`, `spanFinrank_bot`, `spanFinrank_eq_iInf`, `spanFinrank_eq_zero_iff_eq_bot`, `spanFinrank_map_le_of_fg`, `spanFinrank_of_not_fg`, `spanFinrank_singleton`, `spanFinrank_span_le_encard`, `spanFinrank_span_le_ncard_of_finite`, `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`	39
Total	42

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`spanFinrank_map_le_of_fg` 📖	mathematical	`FG`	`Submodule.spanFinrank` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `map` `RingHom` `RingHom.instFunLike`	—	`Cardinal.toNat_le_iff_le_of_lt_aleph0` `Submodule.spanRank_finite_iff_fg` `FG.map` `spanRank_map_le`
`spanRank_map_le` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `Submodule.spanRank` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `map` `RingHom` `RingHom.instFunLike`	—	`Submodule.generators_card` `Submodule.FG.spanRank_le_iff_exists_span_set_card_le` `Cardinal.mk_image_le` `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`

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	20 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`, `spanFinrank_span_le_encard`, `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`, `spanFinrank_singleton`, `FG.generators_ncard`, `height_le_ringKrullDim_quotient_add_spanFinrank`, `spanFinrank_eq_zero_iff_eq_bot`, `spanFinrank_bot`, `ringKrullDim_le_ringKrullDim_add_spanFinrank`, `spanFinrank_of_not_fg`, `Ideal.height_le_height_add_spanFinrank_of_le`, `spanFinrank_map_le_of_fg`, `FG.exists_span_set_encard_eq_spanFinrank`, `spanFinrank_eq_iInf`
`spanRank` 📖	CompOp	30 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`, `rank_le_spanRank`, `spanRank_range_le`, `spanRank_span_of_linearIndepOn`, `spanRank_span_le_card`, `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`, `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`, `spanRank_eq_zero_iff_eq_bot`, `spanRank_top`, `Ideal.exists_spanRank_eq_and_height_eq`, `Ideal.height_le_spanRank_toENat`, `Module.Basis.mk_eq_spanRank`, `spanRank_eq_of_equiv`, `FG.spanRank_le_iff_exists_span_set_card_le`, `spanRank_bot`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_span_set_card_eq_spanRank` 📖	mathematical	—	`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`
`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_le_of_fg` 📖	mathematical	`FG`	`spanFinrank` `map`	—	`Cardinal.toNat_le_iff_le_of_lt_aleph0` `spanRank_finite_iff_fg` `FG.map` `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` `spanFinrank_eq_zero_iff_eq_bot` `fg_span_singleton`
`spanFinrank_span_le_encard` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `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` `IsOrderedRing.toZeroLEOneClass` `le_trans` `spanFinrank_span_le_encard` `Eq.ge` `Set.Finite.cast_ncard_eq`
`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`	—	`LE.le.antisymm` `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` `le_imp_le_of_le_of_le` `spanRank_span_le_card` `le_refl` `Cardinal.mk_image_eq` `span_image` `map_injective_of_injective`
`spanRank_map_le` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `spanRank` `map`	—	`generators_card` `FG.spanRank_le_iff_exists_span_set_card_le` `Cardinal.mk_image_le` `le_antisymm` `span_le` `subset_span` `span_generators` `span_image` `map.congr_simp`
`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` `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` `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` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `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` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `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` `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.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_le_iff_exists_span_set_card_le` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `Submodule.spanRank` `Set.Elem` `Submodule.span`	—	`Submodule.exists_span_set_card_eq_spanRank` `le_trans` `Submodule.spanRank_span_le_card`

---

← Back to Index