Documentation Verification Report

StrongRankCondition

📁 Source: Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean

Statistics

Metric	Count
Definitions `IsQuadraticExtension`, `indexEquiv`, `unique`, `instFintypeElemExtendOfFiniteSubtypeMemSubmoduleSpan`, `inductionOnRank`	5
Theorems `finrank_eq_two`, `finrank_eq_two'`, `toFree`, `card_le_card_of_linearIndependent_aux`, `le_span''`, `rank_eq`, `finite_of_le_span_finite`, `finrank_le_finrank_of_injective`, `finrank_le_of_isSMulRegular`, `finrank_range_le`, `card_le_card_of_le`, `card_le_card_of_linearIndependent`, `card_le_card_of_submodule`, `le_span`, `mk_eq_rank`, `mk_eq_rank'`, `mk_eq_rank''`, `mk_range_eq_rank`, `finrank_bot_le_finrank_of_isScalarTower`, `finrank_eq_card_basis`, `finrank_eq_card_finset_basis`, `finrank_eq_nat_card_basis`, `finrank_eq_rank`, `finrank_eq_zero_iff_of_free`, `finrank_pos_iff_of_free`, `finrank_self`, `finrank_top_le_finrank_of_isScalarTower`, `mk_finrank_eq_card_basis`, `rank_lt_aleph0`, `rank_pos_iff_of_free`, `rank_pos_of_free`, `rank_self`, `rank_zero_iff_of_free`, `of_isNoetherian`, `exists_finset_span_eq_linearIndepOn`, `exists_fun_fin_finrank_span_eq`, `finrank_eq_rank`, `mem_span_set_iff_exists_finsupp_le_finrank`, `basis_le_span'`, `card_le_of_injective''`, `linearIndependent_le_basis`, `linearIndependent_le_infinite_basis`, `linearIndependent_le_span`, `linearIndependent_le_span'`, `linearIndependent_le_span''`, `linearIndependent_le_span_aux'`, `linearIndependent_le_span_finset`, `maximal_linearIndependent_eq_infinite_basis`, `mk_eq_mk_of_basis`, `mk_eq_mk_of_basis'`, `rank_eq_card_basis`, `rank_span`, `rank_span_set`, `strongRankCondition_iff_forall_rank_lt_aleph0`, `strongRankCondition_iff_forall_zero_lt_finrank`, `toENat_rank_span_set`	56
Total	61

Algebra

Definitions

Name	Category	Theorems
`IsQuadraticExtension` 📖	CompData	2 math math: `NumberField.IsCMField.isQuadraticExtension`, `NumberField.IsCMField.is_quadratic`

Algebra.IsQuadraticExtension

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finrank_eq_two` 📖	mathematical	—	`Module.finrank` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule`	—	`finrank_eq_two'`
`finrank_eq_two'` 📖	mathematical	—	`Module.finrank` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule`	—	—
`toFree` 📖	mathematical	—	`Module.Free` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule`	—	—

Basis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_le_card_of_linearIndependent_aux` 📖	—	`LinearIndependent` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Pi.Function.module` `Semiring.toModule`	—	—	`Cardinal.mk_fintype` `Fintype.card_fin` `Cardinal.addLeftMono` `IsOrderedRing.toZeroLEOneClass` `Cardinal.isOrderedRing` `Cardinal.instCharZero` `linearIndependent_le_basis` `Finite.of_fintype`
`le_span''` 📖	mathematical	`Submodule.span` `Top.top` `Submodule` `Submodule.instTop`	`Fintype.card` `Set.Elem`	—	`card_le_of_surjective'` `RingHomCompTriple.ids` `RingHomInvPair.ids` `LinearEquiv.surjective` `RingHomSurjective.ids` `LinearMap.range_eq_top` `Finsupp.range_linearCombination` `Subtype.range_coe_subtype`

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`rank_eq` 📖	mathematical	—	`Fintype.card`	—	`IsScalarTower.right` `Submodule.nonzero_mem_of_bot_lt` `bot_lt_iff_ne_bot` `IsScalarTower.left` `Module.Basis.linearIndependent` `Fintype.linearIndependent_iff` `Finset.sum_congr` `Submodule.isScalarTower'` `instIsTorsionFreeSubtypeMemSubmodule` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `NoZeroDivisors.toNoZeroSMulDivisors` `IsDomain.to_noZeroDivisors` `IsDomain.toIsCancelMulZero` `le_antisymm` `Module.Basis.card_le_card_of_linearIndependent` `LinearMap.IsScalarTower.compatibleSMul` `LinearIndependent.map'` `LinearMap.ker_eq_bot` `Subtype.coe_injective`

LinearIndependent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_of_le_span_finite` 📖	mathematical	`LinearIndependent` `Set` `Set.instLE` `Set.range` `SetLike.coe` `Submodule` `Submodule.setLike` `Submodule.span`	`Finite`	—	`Fintype.finite` `comp` `Subtype.val_injective` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.range_comp_subset_range` `Fintype.card_coe` `linearIndependent_le_span_aux'`

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finrank_le_finrank_of_injective` 📖	mathematical	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instFunLike`	`Module.finrank`	—	`Module.finrank_le_finrank_of_rank_le_rank` `lift_rank_le_of_injective` `Module.rank_lt_aleph0`
`finrank_le_of_isSMulRegular` 📖	mathematical	`IsSMulRegular` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Module.toDistribMulAction` `Submodule` `SetLike.instMembership` `Submodule.setLike`	`Module.finrank` `Submodule.addCommMonoid` `Submodule.module`	—	`Module.finrank_le_finrank_of_rank_le_rank` `Cardinal.lift_le` `rank_le_of_isSMulRegular` `Module.finrank_eq_rank` `Cardinal.natCast_lt_aleph0`
`finrank_range_le` 📖	mathematical	—	`Module.finrank` `Submodule` `SetLike.instMembership` `Submodule.setLike` `range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `Submodule.addCommMonoid` `Submodule.module`	—	`Module.finrank_le_finrank_of_rank_le_rank` `RingHomSurjective.ids` `lift_rank_range_le` `Module.rank_lt_aleph0`

Module

Definitions

Name	Category	Theorems
`instFintypeElemExtendOfFiniteSubtypeMemSubmoduleSpan` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finrank_bot_le_finrank_of_isScalarTower` 📖	mathematical	—	`finrank` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`finrank_le_finrank_of_rank_le_rank` `lift_rank_bot_le_lift_rank_of_isScalarTower` `rank_lt_aleph0`
`finrank_eq_card_basis` 📖	mathematical	—	`finrank` `Fintype.card`	—	`finrank_eq_of_rank_eq` `rank_eq_card_basis`
`finrank_eq_card_finset_basis` 📖	mathematical	—	`finrank` `Finset.card`	—	`finrank_eq_card_basis` `Fintype.card_coe`
`finrank_eq_nat_card_basis` 📖	mathematical	—	`finrank` `Nat.card`	—	`Nat.card.eq_1` `Cardinal.toNat_lift` `Basis.mk_eq_rank` `finrank.eq_1`
`finrank_eq_rank` 📖	mathematical	—	`Cardinal` `Cardinal.instNatCast` `finrank` `rank`	—	`finrank.eq_1` `Cardinal.cast_toNat_of_lt_aleph0` `rank_lt_aleph0`
`finrank_eq_zero_iff_of_free` 📖	mathematical	—	`finrank`	—	`rank_lt_aleph0` `not_le`
`finrank_pos_iff_of_free` 📖	mathematical	—	`finrank` `Nontrivial`	—	`not_subsingleton_iff_nontrivial` `iff_not_comm` `Nat.instCanonicallyOrderedAdd`
`finrank_self` 📖	mathematical	—	`finrank` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`finrank_eq_of_rank_eq` `rank_self` `Nat.cast_one`
`finrank_top_le_finrank_of_isScalarTower` 📖	mathematical	—	`finrank`	—	`finrank.eq_1` `Cardinal.toNat_le_iff_le_of_lt_aleph0` `lt_of_le_of_lt` `rank_top_le_rank_of_isScalarTower` `rank_lt_aleph0`
`mk_finrank_eq_card_basis` 📖	mathematical	—	`Cardinal` `Cardinal.instNatCast` `finrank`	—	`nonempty_fintype` `Finite.finite_basis` `nontrivial_of_invariantBasisNumber` `invariantBasisNumber_of_rankCondition` `rankCondition_of_strongRankCondition` `Cardinal.mk_fintype` `finrank_eq_card_basis`
`rank_lt_aleph0` 📖	mathematical	—	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder` `rank` `Cardinal.aleph0`	—	`rank_def` `finite_def` `LE.le.trans_lt` `ciSup_le'` `linearIndependent_le_span_finset` `Subtype.prop` `Cardinal.natCast_lt_aleph0`
`rank_pos_iff_of_free` 📖	mathematical	—	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder` `Cardinal.instZero` `rank` `Nontrivial`	—	`not_subsingleton_iff_nontrivial` `rank_subsingleton'` `nontrivial_of_invariantBasisNumber` `invariantBasisNumber_of_rankCondition` `rankCondition_of_strongRankCondition` `rank_pos_of_free`
`rank_pos_of_free` 📖	mathematical	—	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder` `Cardinal.instZero` `rank`	—	`nontrivial` `LT.lt.trans_le` `pos_of_ne_zero` `Cardinal.canonicallyOrderedAdd` `Cardinal.mk_ne_zero` `Free.instNonemptyChooseBasisIndexOfNontrivial` `LinearIndependent.cardinal_le_rank` `Basis.linearIndependent`
`rank_self` 📖	mathematical	—	`rank` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Cardinal` `Cardinal.instOne`	—	`Basis.mk_eq_rank` `Cardinal.mk_punit`
`rank_zero_iff_of_free` 📖	mathematical	—	`rank` `Cardinal` `Cardinal.instZero`	—	`not_nontrivial_iff_subsingleton` `iff_not_comm` `rank_pos_iff_of_free` `pos_iff_ne_zero` `Cardinal.canonicallyOrderedAdd`

Module.Basis

Definitions

Name	Category	Theorems
`indexEquiv` 📖	CompOp	—
`unique` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_le_card_of_le` 📖	mathematical	`Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder`	`Fintype.card`	—	`card_le_card_of_linearIndependent` `LinearIndependent.map_injOn` `linearIndependent` `Function.Injective.injOn` `Submodule.inclusion_injective`
`card_le_card_of_linearIndependent` 📖	mathematical	`LinearIndependent`	`Fintype.card`	—	`Cardinal.mk_fintype` `Cardinal.lift_natCast` `rank_eq_card_basis` `Cardinal.addLeftMono` `IsOrderedRing.toZeroLEOneClass` `Cardinal.isOrderedRing` `Cardinal.instCharZero` `LinearIndependent.cardinal_lift_le_rank` `nontrivial_of_invariantBasisNumber` `invariantBasisNumber_of_rankCondition` `rankCondition_of_strongRankCondition`
`card_le_card_of_submodule` 📖	mathematical	—	`Fintype.card`	—	`card_le_card_of_linearIndependent` `LinearIndependent.map_injOn` `linearIndependent` `Function.Injective.injOn` `Submodule.injective_subtype`
`le_span` 📖	mathematical	`Submodule.span` `Top.top` `Submodule` `Submodule.instTop`	`Cardinal` `Cardinal.instLE` `Set.Elem` `Set.range` `DFunLike.coe` `Module.Basis` `instFunLike`	—	`Cardinal.lift_le` `Cardinal.mk_range_eq_of_injective` `injective` `nontrivial_of_invariantBasisNumber` `invariantBasisNumber_of_rankCondition` `Cardinal.mk_fintype` `Cardinal.lift_natCast` `basis_le_span'` `RingHomInvPair.ids` `Set.mem_range` `Submodule.span_le` `Set.mem_iUnion` `Finsupp.support_single_ne_zero` `one_ne_zero` `NeZero.one` `Finsupp.mem_supported` `repr_self` `Finset.mem_singleton_self` `Set.mem_image` `le_of_not_gt` `lt_of_le_of_lt` `le_trans` `Cardinal.sum_le_sum` `LT.lt.le` `Cardinal.lt_aleph0_of_finite` `Finite.Set.finite_image` `Finite.of_fintype` `Cardinal.sum_const` `Cardinal.lift_id` `Cardinal.mul_aleph0_eq` `not_le_of_gt`
`mk_eq_rank` 📖	mathematical	—	`Cardinal.lift` `Module.rank`	—	`mk_range_eq_rank` `Cardinal.mk_range_eq_of_injective` `injective` `nontrivial_of_invariantBasisNumber` `invariantBasisNumber_of_rankCondition` `rankCondition_of_strongRankCondition`
`mk_eq_rank'` 📖	mathematical	—	`Cardinal.lift` `Module.rank`	—	`Cardinal.lift_umax_eq` `mk_eq_rank`
`mk_eq_rank''` 📖	mathematical	—	`Module.rank`	—	`Module.rank_def` `le_antisymm` `LinearIndepOn.eq_1` `reindexRange_apply` `linearIndependent` `Eq.ge` `Cardinal.mk_range_eq` `injective` `nontrivial_of_invariantBasisNumber` `invariantBasisNumber_of_rankCondition` `rankCondition_of_strongRankCondition` `le_ciSup` `Cardinal.bddAbove_range` `small_subtype` `small_set` `UnivLE.small` `UnivLE.self` `ciSup_le'` `linearIndependent_le_basis`
`mk_range_eq_rank` 📖	mathematical	—	`Set.Elem` `Set.range` `DFunLike.coe` `Module.Basis` `instFunLike` `Module.rank`	—	`mk_eq_rank''`

StrongRankCondition

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_isNoetherian` 📖	mathematical	`IsNoetherian` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Pi.Function.module` `Semiring.toModule`	`StrongRankCondition`	—	`strongRankCondition_iff_succ` `RingHomInvPair.ids` `RingHomCompTriple.ids` `not_subsingleton` `IsNoetherian.subsingleton_of_injective` `LinearEquiv.injective`

Submodule

Definitions

Name	Category	Theorems
`inductionOnRank` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_finset_span_eq_linearIndepOn` 📖	mathematical	—	`Set` `Set.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.card` `Module.finrank` `Submodule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `span` `addCommMonoid` `module` `LinearIndepOn`	—	`exists_linearIndependent` `Cardinal.mk_set_eq_nat_iff_finset` `Module.finrank_eq_rank` `IsNoetherianRing.strongRankCondition` `DivisionRing.toNontrivial` `PrincipalIdealRing.isNoetherianRing` `DivisionSemiring.isPrincipalIdealRing` `rank_span_set`
`exists_fun_fin_finrank_span_eq` 📖	mathematical	—	`Set` `Set.instMembership` `span` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Set.range` `Module.finrank` `Submodule` `SetLike.instMembership` `setLike` `addCommMonoid` `module` `LinearIndependent`	—	`exists_finset_span_eq_linearIndepOn` `EquivLike.range_comp` `Subtype.range_coe_subtype` `LinearIndependent.comp` `Equiv.injective`
`finrank_eq_rank` 📖	mathematical	—	`Cardinal` `Cardinal.instNatCast` `Module.finrank` `Submodule` `SetLike.instMembership` `setLike` `addCommMonoid` `module` `Module.rank`	—	`Module.finrank.eq_1` `Cardinal.cast_toNat_of_lt_aleph0` `lt_of_le_of_lt` `rank_le` `Module.rank_lt_aleph0`
`mem_span_set_iff_exists_finsupp_le_finrank` 📖	mathematical	—	`Submodule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `span` `Finset.card` `Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DivisionRing.toRing` `Module.finrank` `addCommMonoid` `module` `Set` `Set.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike` `Finsupp.sum` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`exists_finset_span_eq_linearIndepOn` `mem_span_set` `Finset.card_mono` `HasSubset.Subset.trans` `Set.instIsTransSubset`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`basis_le_span'` 📖	mathematical	`Submodule.span` `Top.top` `Submodule` `Submodule.instTop`	`Cardinal` `Cardinal.instLE` `Cardinal.instNatCast` `Fintype.card` `Set.Elem`	—	`nonempty_fintype` `basis_finite_of_finite_spans` `nontrivial_of_invariantBasisNumber` `invariantBasisNumber_of_rankCondition` `Set.toFinite` `Finite.of_fintype` `Cardinal.mk_fintype` `Cardinal.addLeftMono` `IsOrderedRing.toZeroLEOneClass` `Cardinal.isOrderedRing` `Cardinal.instCharZero` `Basis.le_span''`
`card_le_of_injective''` 📖	mathematical	`Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DFunLike.coe` `LinearMap` `RingHom.id` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `LinearMap.instFunLike`	`Cardinal` `Cardinal.instLE`	—	`RingHomInvPair.ids` `linearIndependent_le_basis` `LinearIndependent.eq_1` `Finsupp.lhom_ext'` `LinearMap.ext_ring` `RingHomCompTriple.ids` `Finsupp.ext` `Finsupp.linearCombination_single` `one_smul`
`linearIndependent_le_basis` 📖	mathematical	`LinearIndependent`	`Cardinal` `Cardinal.instLE`	—	`Cardinal.mk_fintype` `Fintype.card_congr` `Module.Basis.injective` `nontrivial_of_invariantBasisNumber` `invariantBasisNumber_of_rankCondition` `rankCondition_of_strongRankCondition` `linearIndependent_le_span` `Module.Basis.span_eq` `linearIndependent_le_infinite_basis`
`linearIndependent_le_infinite_basis` 📖	mathematical	`LinearIndependent`	`Cardinal` `Cardinal.instLE`	—	`RingHomInvPair.ids` `Cardinal.exists_infinite_fiber` `Cardinal.mk_finset_of_infinite` `not_le` `instInfiniteFinset` `LinearIndependent.comp` `Subtype.val_injective` `LinearIndependent.finite_of_le_span_finite` `Finite.of_fintype` `Finset.coe_image` `Module.Basis.mem_span_repr_support` `Infinite.false`
`linearIndependent_le_span` 📖	mathematical	`LinearIndependent` `Submodule.span` `Top.top` `Submodule` `Submodule.instTop`	`Cardinal` `Cardinal.instLE` `Cardinal.instNatCast` `Fintype.card` `Set.Elem`	—	`linearIndependent_le_span'` `le_top`
`linearIndependent_le_span'` 📖	mathematical	`LinearIndependent` `Set` `Set.instLE` `Set.range` `SetLike.coe` `Submodule` `Submodule.setLike` `Submodule.span`	`Cardinal` `Cardinal.instLE` `Cardinal.instNatCast` `Fintype.card` `Set.Elem`	—	`LinearIndependent.finite_of_le_span_finite` `Finite.of_fintype` `Cardinal.mk_fintype` `Cardinal.addLeftMono` `IsOrderedRing.toZeroLEOneClass` `Cardinal.isOrderedRing` `Cardinal.instCharZero` `linearIndependent_le_span_aux'`
`linearIndependent_le_span''` 📖	mathematical	`LinearIndependent` `Submodule.span` `Top.top` `Submodule` `Submodule.instTop`	`Cardinal` `Cardinal.instLE` `Set.Elem`	—	`card_le_of_injective''` `Finsupp.linearCombination_linearCombination` `Span.finsupp_linearCombination_repr`
`linearIndependent_le_span_aux'` 📖	mathematical	`LinearIndependent` `Set` `Set.instLE` `Set.range` `SetLike.coe` `Submodule` `Submodule.setLike` `Submodule.span`	`Fintype.card` `Set.Elem`	—	`card_le_of_injective'` `Set.mem_range_self` `Finsupp.linearCombination_linearCombination` `Span.finsupp_linearCombination_repr`
`linearIndependent_le_span_finset` 📖	mathematical	`LinearIndependent` `Submodule.span` `SetLike.coe` `Finset` `Finset.instSetLike` `Top.top` `Submodule` `Submodule.instTop`	`Cardinal` `Cardinal.instLE` `Cardinal.instNatCast` `Finset.card`	—	`Fintype.card_coe` `linearIndependent_le_span`
`maximal_linearIndependent_eq_infinite_basis` 📖	—	`LinearIndependent` `LinearIndependent.Maximal`	—	—	`le_antisymm` `linearIndependent_le_basis` `infinite_basis_le_maximal_linearIndependent` `nontrivial_of_invariantBasisNumber` `invariantBasisNumber_of_rankCondition` `rankCondition_of_strongRankCondition`
`mk_eq_mk_of_basis` 📖	mathematical	—	`Cardinal.lift`	—	`nonempty_fintype` `basis_finite_of_finite_spans` `nontrivial_of_invariantBasisNumber` `Set.finite_range` `Finite.of_fintype` `Module.Basis.span_eq` `Cardinal.mk_fintype` `Cardinal.lift_natCast` `Cardinal.instCharZero` `card_eq_of_linearEquiv` `RingHomCompTriple.ids` `RingHomInvPair.ids` `infinite_basis_le_maximal_linearIndependent'` `Module.Basis.linearIndependent` `Module.Basis.maximal` `Cardinal.lift_mk_le'` `Infinite.of_injective` `Function.Embedding.inj'` `le_antisymm`
`mk_eq_mk_of_basis'` 📖	—	—	—	—	`mk_eq_mk_of_basis`
`rank_eq_card_basis` 📖	mathematical	—	`Module.rank` `Cardinal` `Cardinal.instNatCast` `Fintype.card`	—	`Module.Basis.mk_range_eq_rank` `Cardinal.mk_fintype` `Set.card_range_of_injective` `Module.Basis.injective` `nontrivial_of_invariantBasisNumber` `invariantBasisNumber_of_rankCondition` `rankCondition_of_strongRankCondition`
`rank_span` 📖	mathematical	`LinearIndependent`	`Module.rank` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.range` `Submodule.addCommMonoid` `Submodule.module` `Set.Elem`	—	`Module.Basis.mk_eq_rank` `Cardinal.mk_range_eq_of_injective` `LinearIndependent.injective` `nontrivial_of_invariantBasisNumber` `invariantBasisNumber_of_rankCondition` `rankCondition_of_strongRankCondition`
`rank_span_set` 📖	mathematical	`LinearIndepOn`	`Module.rank` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Submodule.addCommMonoid` `Submodule.module` `Set.Elem`	—	`Set.setOf_mem_eq` `Subtype.range_coe_subtype` `rank_span`
`strongRankCondition_iff_forall_rank_lt_aleph0` 📖	mathematical	—	`StrongRankCondition` `Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder` `Module.rank` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Pi.Function.module` `Semiring.toModule` `Cardinal.aleph0`	—	`strongRankCondition_iff_succ` `not_iff_not` `Mathlib.Tactic.Push.not_forall_eq` `LinearMap.exists_finsupp_nat_of_fin_fun_injective` `Cardinal.lift_uzero` `LinearIndependent.cardinal_lift_le_rank` `LinearIndependent.map_injOn` `Module.Basis.linearIndependent` `Function.Injective.injOn` `Module.le_rank_iff_exists_linearMap` `LE.le.trans` `Cardinal.natCast_le_aleph0`
`strongRankCondition_iff_forall_zero_lt_finrank` 📖	mathematical	—	`StrongRankCondition` `Module.finrank` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Pi.Function.module` `Semiring.toModule`	—	`strongRankCondition_iff_forall_rank_lt_aleph0` `not_iff_not` `Mathlib.Tactic.Push.not_forall_eq` `LE.le.trans` `LinearMap.rank_le_of_injective` `Function.extend_injective` `Fin.castSucc_injective` `Module.one_le_rank_iff` `Cardinal.one_le_iff_ne_zero` `Pi.single_injective`
`toENat_rank_span_set` 📖	mathematical	`LinearIndepOn`	`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` `Module.rank` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.image` `Submodule.addCommMonoid` `Submodule.module` `Set.encard`	—	`Set.image_eq_range` `Set.InjOn.encard_image` `LinearIndepOn.injOn` `nontrivial_of_invariantBasisNumber` `invariantBasisNumber_of_rankCondition` `rankCondition_of_strongRankCondition` `Set.toENat_cardinalMk` `rank_span` `LinearIndepOn.linearIndependent`

---

← Back to Index