Documentation Verification Report

Lemmas

📁 Source: Mathlib/LinearAlgebra/FiniteDimensional/Lemmas.lean

Statistics

Metric	Count
Definitions `quotEquivOfEquiv`, `quotEquivOfQuotEquiv`, `linearEquivOfInjective`, `basisOfLinearIndependentOfCardEqFinrank`, `basisOfPiSpaceOfLinearIndependent`, `finsetBasisOfLinearIndependentOfCardEqFinrank`, `setBasisOfLinearIndependentOfCardEqFinrank`	7
Theorems `span_eq_top_of_card_eq_finrank`, `span_eq_top_of_card_eq_finrank'`, `finrank_range_add_finrank_ker`, `injective_iff_surjective_of_finrank_eq_finrank`, `ker_eq_bot_iff_range_eq_top_of_finrank_eq_finrank`, `ker_ne_bot_of_finrank_lt`, `linearEquivOfInjective_apply`, `exists_ker_pow_eq_ker_pow_succ`, `ker_pow_eq_ker_pow_finrank_of_le`, `ker_pow_le_ker_pow_finrank`, `isSimpleOrder_of_finrank`, `eq_top_of_disjoint`, `finrank_add_eq_of_isCompl`, `finrank_add_finrank_le_of_disjoint`, `finrank_add_le_finrank_add_finrank`, `finrank_lt`, `finrank_lt_finrank_of_lt`, `finrank_strictMono`, `finrank_sup_add_finrank_inf_eq`, `isCompl_iff_disjoint`, `basisOfLinearIndependentOfCardEqFinrank_repr_apply`, `coe_basisOfLinearIndependentOfCardEqFinrank`, `coe_basisOfPiSpaceOfLinearIndependent`, `coe_finsetBasisOfLinearIndependentOfCardEqFinrank`, `coe_setBasisOfLinearIndependentOfCardEqFinrank`, `finsetBasisOfLinearIndependentOfCardEqFinrank_repr_apply`, `is_simple_module_of_finrank_eq_one`, `setBasisOfLinearIndependentOfCardEqFinrank_repr_apply`	28
Total	35

FiniteDimensional.LinearEquiv

Definitions

Name	Category	Theorems
`quotEquivOfEquiv` 📖	CompOp	—
`quotEquivOfQuotEquiv` 📖	CompOp	—

LinearIndependent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`span_eq_top_of_card_eq_finrank` 📖	mathematical	`LinearIndependent` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Fintype.card` `Module.finrank`	`Submodule.span` `Set.range` `Top.top` `Submodule` `Submodule.instTop`	—	`FiniteDimensional.of_finrank_pos` `Fintype.card_pos` `span_eq_top_of_card_eq_finrank'`
`span_eq_top_of_card_eq_finrank'` 📖	mathematical	`LinearIndependent` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Fintype.card` `Module.finrank`	`Submodule.span` `Set.range` `Top.top` `Submodule` `Submodule.instTop`	—	`ne_of_lt` `Submodule.finrank_lt` `finrank_span_eq_card` `IsNoetherianRing.strongRankCondition` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `PrincipalIdealRing.isNoetherianRing` `DivisionSemiring.isPrincipalIdealRing`

LinearMap

Definitions

Name	Category	Theorems
`linearEquivOfInjective` 📖	CompOp	1 math math: `linearEquivOfInjective_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finrank_range_add_finrank_ker` 📖	mathematical	—	`Module.finrank` `Submodule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `Submodule.addCommMonoid` `Submodule.module` `ker`	—	`RingHomSurjective.ids` `LinearEquiv.finrank_eq` `Submodule.finrank_quotient_add_finrank` `DivisionRing.hasRankNullity` `IsNoetherianRing.strongRankCondition` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `PrincipalIdealRing.isNoetherianRing` `DivisionSemiring.isPrincipalIdealRing`
`injective_iff_surjective_of_finrank_eq_finrank` 📖	mathematical	`Module.finrank` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid`	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instFunLike`	—	`RingHomSurjective.ids` `finrank_range_add_finrank_ker` `ker_eq_bot` `range_eq_top` `Submodule.eq_top_of_finrank_eq` `add_zero` `finrank_bot` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `Submodule.finrank_eq_zero` `DivisionRing.isDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `IsNoetherianRing.strongRankCondition` `PrincipalIdealRing.isNoetherianRing` `DivisionSemiring.isPrincipalIdealRing` `FiniteDimensional.finiteDimensional_submodule` `add_right_injective` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `finrank_top`
`ker_eq_bot_iff_range_eq_top_of_finrank_eq_finrank` 📖	mathematical	`Module.finrank` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid`	`ker` `RingHom.id` `Semiring.toNonAssocSemiring` `Bot.bot` `Submodule` `Submodule.instBot` `range` `RingHomSurjective.ids` `Top.top` `Submodule.instTop`	—	`RingHomSurjective.ids` `range_eq_top` `ker_eq_bot` `injective_iff_surjective_of_finrank_eq_finrank`
`ker_ne_bot_of_finrank_lt` 📖	—	`Module.finrank` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid`	—	—	`RingHomSurjective.ids` `finrank_range_add_finrank_ker` `Submodule.finrank_le` `IsNoetherianRing.strongRankCondition` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `PrincipalIdealRing.isNoetherianRing` `DivisionSemiring.isPrincipalIdealRing` `Submodule.one_le_finrank_iff` `DivisionRing.isDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `FiniteDimensional.finiteDimensional_submodule`
`linearEquivOfInjective_apply` 📖	mathematical	`DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike` `Module.finrank`	`LinearEquiv` `RingHomInvPair.ids` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `linearEquivOfInjective`	—	`RingHomInvPair.ids`

Module.End

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_ker_pow_eq_ker_pow_succ` 📖	mathematical	—	`Module.finrank` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.ker` `RingHom.id` `Semiring.toNonAssocSemiring` `Module.End` `Monoid.toNatPow` `instMonoid`	—	`zero_le` `Nat.instCanonicallyOrderedAdd` `lt_of_le_of_ne` `pow_succ'` `LinearMap.ker_le_ker_comp` `Submodule.finrank_lt_finrank_of_lt` `FiniteDimensional.finiteDimensional_submodule` `LE.le.trans` `Submodule.finrank_le` `IsNoetherianRing.strongRankCondition` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `PrincipalIdealRing.isNoetherianRing` `DivisionSemiring.isPrincipalIdealRing`
`ker_pow_eq_ker_pow_finrank_of_le` 📖	mathematical	`Module.finrank` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid`	`LinearMap.ker` `RingHom.id` `Semiring.toNonAssocSemiring` `Module.End` `Monoid.toNatPow` `instMonoid`	—	`exists_ker_pow_eq_ker_pow_succ` `add_tsub_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `LE.le.trans` `ker_pow_constant`
`ker_pow_le_ker_pow_finrank` 📖	mathematical	—	`Submodule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `LinearMap.ker` `RingHom.id` `Semiring.toNonAssocSemiring` `Module.End` `Monoid.toNatPow` `instMonoid` `Module.finrank`	—	`add_tsub_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `LT.lt.le` `add_comm` `pow_add` `LinearMap.ker_le_ker_comp` `ker_pow_eq_ker_pow_finrank_of_le` `le_refl`

Subalgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSimpleOrder_of_finrank` 📖	mathematical	`Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `Semifield.toCommSemiring` `Ring.toSemiring`	`IsSimpleOrder` `Subalgebra` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `CompleteLattice.toBoundedOrder` `Algebra.instCompleteLatticeSubalgebra`	—	`Module.nontrivial_of_finrank_pos` `EuclideanDomain.toNontrivial` `LT.lt.trans_eq` `Nat.instAtLeastTwoHAddOfNat` `zero_lt_two` `Nat.instZeroLEOneClass` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `bot_eq_top_iff_finrank_eq_one` `IsNoetherianRing.strongRankCondition` `PrincipalIdealRing.isNoetherianRing` `EuclideanDomain.to_principal_ideal_domain` `Module.Free.of_divisionRing` `Submodule.finrank_le` `FiniteDimensional.of_finrank_eq_succ` `Module.finrank_pos_iff` `FiniteDimensional.finiteDimensional_submodule` `instIsDomain` `instIsTorsionFree` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `SubsemiringClass.nontrivial` `instSubsemiringClass` `Algebra.toSubmodule_eq_top` `Submodule.eq_top_of_finrank_eq` `le_antisymm` `Mathlib.Tactic.IntervalCases.of_le_right` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_ofNat` `eq_bot_of_finrank_one` `Mathlib.Tactic.IntervalCases.of_lt_left`

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_top_of_disjoint` 📖	mathematical	`Module.finrank` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Submodule` `SetLike.instMembership` `setLike` `addCommMonoid` `module` `Disjoint` `instPartialOrder` `instOrderBot`	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice` `Top.top` `instTop`	—	`le_bot_iff` `disjoint_iff_inf_le` `finrank_bot` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `eq_top_of_finrank_eq` `le_antisymm` `finrank_add_finrank_le_of_disjoint` `finrank_sup_add_finrank_inf_eq` `FiniteDimensional.finiteDimensional_submodule`
`finrank_add_eq_of_isCompl` 📖	mathematical	`IsCompl` `Submodule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `instPartialOrder` `CompleteLattice.toBoundedOrder` `completeLattice`	`Module.finrank` `SetLike.instMembership` `setLike` `addCommMonoid` `module`	—	`finrank_sup_add_finrank_inf_eq` `FiniteDimensional.finiteDimensional_submodule` `Codisjoint.eq_top` `IsCompl.codisjoint` `Disjoint.eq_bot` `IsCompl.disjoint` `finrank_bot` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `add_zero` `finrank_top`
`finrank_add_finrank_le_of_disjoint` 📖	mathematical	`Disjoint` `Submodule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `instPartialOrder` `instOrderBot`	`Module.finrank` `SetLike.instMembership` `setLike` `addCommMonoid` `module`	—	`finrank_sup_add_finrank_inf_eq` `FiniteDimensional.finiteDimensional_submodule` `Disjoint.eq_bot` `finrank_bot` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `add_zero` `finrank_le` `IsNoetherianRing.strongRankCondition` `PrincipalIdealRing.isNoetherianRing` `DivisionSemiring.isPrincipalIdealRing`
`finrank_add_le_finrank_add_finrank` 📖	mathematical	—	`Module.finrank` `Submodule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice` `addCommMonoid` `module`	—	`finrank_sup_add_finrank_inf_eq` `self_le_add_right` `Nat.instCanonicallyOrderedAdd`
`finrank_lt` 📖	mathematical	—	`Module.finrank` `Submodule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `addCommMonoid` `module`	—	`finrank_quotient_add_finrank` `DivisionRing.hasRankNullity` `IsNoetherianRing.strongRankCondition` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `PrincipalIdealRing.isNoetherianRing` `DivisionSemiring.isPrincipalIdealRing` `add_comm` `Module.finrank_pos` `FiniteDimensional.finiteDimensional_quotient` `DivisionRing.isDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `Quotient.nontrivial_iff`
`finrank_lt_finrank_of_lt` 📖	mathematical	`Submodule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder`	`Module.finrank` `SetLike.instMembership` `setLike` `addCommMonoid` `module`	—	`Eq.trans_lt` `LinearEquiv.finrank_eq` `LT.lt.le` `finrank_lt` `not_le_of_gt`
`finrank_strictMono` 📖	mathematical	—	`StrictMono` `Submodule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `PartialOrder.toPreorder` `instPartialOrder` `Nat.instPreorder` `Module.finrank` `SetLike.instMembership` `setLike` `addCommMonoid` `module`	—	`finrank_lt_finrank_of_lt` `FiniteDimensional.finiteDimensional_submodule`
`finrank_sup_add_finrank_inf_eq` 📖	mathematical	—	`Module.finrank` `Submodule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice` `addCommMonoid` `module` `instMin`	—	`rank_sup_add_rank_inf_eq` `DivisionRing.hasRankNullity` `Cardinal.instCharZero` `Module.finrank_eq_rank` `IsNoetherianRing.strongRankCondition` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `PrincipalIdealRing.isNoetherianRing` `DivisionSemiring.isPrincipalIdealRing` `finiteDimensional_inf_right` `finiteDimensional_sup`
`isCompl_iff_disjoint` 📖	mathematical	`Module.finrank` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Submodule` `SetLike.instMembership` `setLike` `addCommMonoid` `module`	`IsCompl` `instPartialOrder` `CompleteLattice.toBoundedOrder` `completeLattice` `Disjoint` `instOrderBot`	—	`IsCompl.disjoint` `codisjoint_iff` `eq_top_of_disjoint`

(root)

Definitions

Name	Category	Theorems
`basisOfLinearIndependentOfCardEqFinrank` 📖	CompOp	2 math math: `basisOfLinearIndependentOfCardEqFinrank_repr_apply`, `coe_basisOfLinearIndependentOfCardEqFinrank`
`basisOfPiSpaceOfLinearIndependent` 📖	CompOp	1 math math: `coe_basisOfPiSpaceOfLinearIndependent`
`finsetBasisOfLinearIndependentOfCardEqFinrank` 📖	CompOp	2 math math: `coe_finsetBasisOfLinearIndependentOfCardEqFinrank`, `finsetBasisOfLinearIndependentOfCardEqFinrank_repr_apply`
`setBasisOfLinearIndependentOfCardEqFinrank` 📖	CompOp	2 math math: `setBasisOfLinearIndependentOfCardEqFinrank_repr_apply`, `coe_setBasisOfLinearIndependentOfCardEqFinrank`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`basisOfLinearIndependentOfCardEqFinrank_repr_apply` 📖	mathematical	`LinearIndependent` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Fintype.card` `Module.finrank`	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `Module.Basis.repr` `basisOfLinearIndependentOfCardEqFinrank` `LinearMap` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.range` `Submodule.addCommMonoid` `Submodule.module` `LinearMap.instFunLike` `LinearIndependent.repr` `LinearMap.codRestrict` `LinearMap.id`	—	`RingHomInvPair.ids`
`coe_basisOfLinearIndependentOfCardEqFinrank` 📖	mathematical	`LinearIndependent` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Fintype.card` `Module.finrank`	`DFunLike.coe` `Module.Basis` `Module.Basis.instFunLike` `basisOfLinearIndependentOfCardEqFinrank`	—	—
`coe_basisOfPiSpaceOfLinearIndependent` 📖	mathematical	`LinearIndependent` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DivisionRing.toRing` `Pi.Function.module` `Semiring.toModule`	`DFunLike.coe` `Module.Basis` `Module.Basis.instFunLike` `basisOfPiSpaceOfLinearIndependent`	—	`coe_basisOfLinearIndependentOfCardEqFinrank` `basisOfPiSpaceOfLinearIndependent.eq_1` `IsEmpty.false` `not_nonempty_iff`
`coe_finsetBasisOfLinearIndependentOfCardEqFinrank` 📖	mathematical	`Finset.Nonempty` `LinearIndependent` `Finset` `SetLike.instMembership` `Finset.instSetLike` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Finset.card` `Module.finrank`	`DFunLike.coe` `Module.Basis` `Module.Basis.instFunLike` `finsetBasisOfLinearIndependentOfCardEqFinrank`	—	`coe_basisOfLinearIndependentOfCardEqFinrank`
`coe_setBasisOfLinearIndependentOfCardEqFinrank` 📖	mathematical	`LinearIndependent` `Set` `Set.instMembership` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Finset.card` `Set.toFinset` `Module.finrank`	`DFunLike.coe` `Module.Basis` `Set.Elem` `Module.Basis.instFunLike` `setBasisOfLinearIndependentOfCardEqFinrank`	—	`coe_basisOfLinearIndependentOfCardEqFinrank`
`finsetBasisOfLinearIndependentOfCardEqFinrank_repr_apply` 📖	mathematical	`Finset.Nonempty` `LinearIndependent` `Finset` `SetLike.instMembership` `Finset.instSetLike` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Finset.card` `Module.finrank`	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `Module.Basis.repr` `finsetBasisOfLinearIndependentOfCardEqFinrank` `LinearMap` `Submodule` `Submodule.setLike` `Submodule.span` `Set.range` `Submodule.addCommMonoid` `Submodule.module` `LinearMap.instFunLike` `LinearIndependent.repr` `LinearMap.codRestrict` `LinearMap.id` `Finset.Subtype.fintype`	—	`RingHomInvPair.ids`
`is_simple_module_of_finrank_eq_one` 📖	mathematical	`Module.finrank` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid`	`IsSimpleOrder` `Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice`	—	`Submodule.instNontrivial` `Module.nontrivial_of_finrank_eq_succ` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `Submodule.eq_top_of_finrank_eq` `FiniteDimensional.of_finrank_eq_succ` `LE.le.antisymm` `Submodule.finrank_le` `IsNoetherianRing.strongRankCondition` `PrincipalIdealRing.isNoetherianRing` `DivisionSemiring.isPrincipalIdealRing` `finrank_bot` `Submodule.finrank_strictMono` `Ne.bot_lt`
`setBasisOfLinearIndependentOfCardEqFinrank_repr_apply` 📖	mathematical	`LinearIndependent` `Set` `Set.instMembership` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Finset.card` `Set.toFinset` `Module.finrank`	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Finsupp` `Set.Elem` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `Module.Basis.repr` `setBasisOfLinearIndependentOfCardEqFinrank` `LinearMap` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.range` `Submodule.addCommMonoid` `Submodule.module` `LinearMap.instFunLike` `LinearIndependent.repr` `LinearMap.codRestrict` `LinearMap.id`	—	`RingHomInvPair.ids`

---

← Back to Index