Documentation Verification Report

FreeAndStrongRankCondition

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

Statistics

Metric	Count
Definitions `ofRankEqZero`	1
Theorems `ofRankEqZero_apply`, `finrank_le_one_iff_top_isPrincipal`, `rank_le_one_iff_top_isPrincipal`, `bot_eq_top_iff_finrank_eq_one`, `bot_eq_top_iff_rank_eq_one`, `bot_eq_top_of_finrank_eq_one`, `bot_eq_top_of_rank_eq_one`, `eq_bot_of_finrank_one`, `eq_bot_of_rank_le_one`, `finrank_eq_one_iff`, `rank_eq_one_iff`, `finrank_le_one_iff_isPrincipal`, `rank_le_one_iff_isPrincipal`, `cardinalMk_eq_cardinalMk_field_pow_rank`, `cardinal_lt_aleph0_of_finiteDimensional`, `finrank_eq_one_iff`, `finrank_eq_one_iff'`, `finrank_le_one_iff`, `le_rank_iff_exists_linearIndependent`, `le_rank_iff_exists_linearIndependent_finset`, `lift_cardinalMk_eq_lift_cardinalMk_field_pow_lift_rank`, `rank_eq_one_iff`, `rank_le_one_iff`, `rank_submodule_eq_one_iff`, `rank_submodule_le_one_iff`, `rank_submodule_le_one_iff'`	26
Total	27

Basis

Definitions

Name	Category	Theorems
`ofRankEqZero` 📖	CompOp	1 math math: `ofRankEqZero_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ofRankEqZero_apply` 📖	mathematical	`Module.rank` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Cardinal` `Cardinal.instZero`	`DFunLike.coe` `Module.Basis` `Module.Basis.instFunLike` `ofRankEqZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—

Module

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finrank_le_one_iff_top_isPrincipal` 📖	mathematical	—	`finrank` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.IsPrincipal` `Top.top` `Submodule` `Submodule.instTop`	—	`rank_le_one_iff_top_isPrincipal` `finrank_eq_rank` `Nat.cast_le_one` `Cardinal.addLeftMono` `IsOrderedRing.toZeroLEOneClass` `Cardinal.isOrderedRing` `Cardinal.instCharZero`
`rank_le_one_iff_top_isPrincipal` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `rank` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Cardinal.instOne` `Submodule.IsPrincipal` `Top.top` `Submodule` `Submodule.instTop`	—	`Submodule.rank_le_one_iff_isPrincipal` `Free.of_equiv` `RingHomInvPair.ids` `rank_top`

Subalgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bot_eq_top_iff_finrank_eq_one` 📖	mathematical	—	`Bot.bot` `Subalgebra` `CommRing.toCommSemiring` `Ring.toSemiring` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `Top.top` `OrderTop.toTop` `BoundedOrder.toOrderTop` `Module.finrank` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule`	—	`finrank_top` `subalgebra_top_finrank_eq_submodule_top_finrank` `finrank_eq_one_iff` `Module.Free.of_equiv` `RingHomInvPair.ids`
`bot_eq_top_iff_rank_eq_one` 📖	mathematical	—	`Bot.bot` `Subalgebra` `CommRing.toCommSemiring` `Ring.toSemiring` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `Top.top` `OrderTop.toTop` `BoundedOrder.toOrderTop` `Module.rank` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `Cardinal` `Cardinal.instOne`	—	`rank_top` `rank_eq_one_iff` `Module.Free.of_equiv` `RingHomInvPair.ids`
`bot_eq_top_of_finrank_eq_one` 📖	mathematical	`Module.finrank` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `Ring.toSemiring`	`Bot.bot` `Subalgebra` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `Top.top` `OrderTop.toTop` `BoundedOrder.toOrderTop`	—	`bot_eq_top_iff_finrank_eq_one`
`bot_eq_top_of_rank_eq_one` 📖	mathematical	`Module.rank` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `Ring.toSemiring` `Cardinal` `Cardinal.instOne`	`Bot.bot` `Subalgebra` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `Top.top` `OrderTop.toTop` `BoundedOrder.toOrderTop`	—	`bot_eq_top_iff_rank_eq_one`
`eq_bot_of_finrank_one` 📖	mathematical	`Module.finrank` `Subalgebra` `CommRing.toCommSemiring` `Ring.toSemiring` `SetLike.instMembership` `instSetLike` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `toRing` `instModuleSubtypeMem`	`Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`eq_bot_of_rank_le_one` `Cardinal.toNat_eq_one` `Module.finrank.eq_1` `le_refl`
`eq_bot_of_rank_le_one` 📖	mathematical	`Cardinal` `Cardinal.instLE` `Module.rank` `Subalgebra` `CommRing.toCommSemiring` `Ring.toSemiring` `SetLike.instMembership` `instSetLike` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `toRing` `instModuleSubtypeMem` `Cardinal.instOne`	`Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `subsingleton_of_subsingleton` `Module.Free.exists_basis` `bot_unique` `Algebra.mem_bot` `unique_iff_subsingleton_and_nonempty` `Cardinal.eq_one_iff_unique` `Module.Basis.mk_eq_rank''` `Function.Bijective.surjective` `bijective_algebraMap_of_linearEquiv` `RingHomInvPair.ids` `RingHomCompTriple.ids` `one_ne_zero` `NeZero.one` `AddSubmonoidWithOneClass.toOneMemClass` `SubsemiringClass.addSubmonoidWithOneClass` `instSubsemiringClass` `AddSubmonoidClass.toZeroMemClass` `SubsemiringClass.toAddSubmonoidClass` `Equiv.subsingleton` `Unique.instSubsingleton` `Cardinal.mk_eq_zero_iff` `Cardinal.lt_one_iff_zero` `LE.le.lt_of_ne`
`finrank_eq_one_iff` 📖	mathematical	—	`Module.finrank` `Subalgebra` `CommRing.toCommSemiring` `Ring.toSemiring` `SetLike.instMembership` `instSetLike` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `toRing` `instModuleSubtypeMem` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`rank_eq_one_iff` `Cardinal.toNat_eq_iff` `one_ne_zero`
`rank_eq_one_iff` 📖	mathematical	—	`Module.rank` `Subalgebra` `CommRing.toCommSemiring` `Ring.toSemiring` `SetLike.instMembership` `instSetLike` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `toRing` `instModuleSubtypeMem` `Cardinal` `Cardinal.instOne` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`eq_bot_of_rank_le_one` `Eq.le` `Module.Free.exists_basis` `le_antisymm` `RingHomSurjective.ids` `lift_rank_range_le` `rank_toSubmodule` `Algebra.toSubmodule_bot` `Cardinal.lift_le_one_iff` `Cardinal.lift_one` `Module.rank_self` `Submodule.one_eq_range` `one_ne_zero` `NeZero.one` `AddSubmonoidWithOneClass.toOneMemClass` `SubsemiringClass.addSubmonoidWithOneClass` `instSubsemiringClass` `AddSubmonoidClass.toZeroMemClass` `SubsemiringClass.toAddSubmonoidClass` `Equiv.subsingleton` `RingHomInvPair.ids` `Unique.instSubsingleton` `Cardinal.mk_eq_zero_iff` `Module.Basis.mk_eq_rank''` `Cardinal.lt_one_iff_zero` `not_le`

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finrank_le_one_iff_isPrincipal` 📖	mathematical	—	`Module.finrank` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `addCommMonoid` `module` `IsPrincipal`	—	`rank_le_one_iff_isPrincipal` `Module.finrank_eq_rank` `Nat.cast_le_one` `Cardinal.addLeftMono` `IsOrderedRing.toZeroLEOneClass` `Cardinal.isOrderedRing` `Cardinal.instCharZero`
`rank_le_one_iff_isPrincipal` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `Module.rank` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `addCommMonoid` `module` `Cardinal.instOne` `IsPrincipal`	—	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cardinalMk_eq_cardinalMk_field_pow_rank` 📖	mathematical	—	`Cardinal` `Cardinal.instPowCardinal` `Module.rank` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid`	—	`Cardinal.lift_id` `lift_cardinalMk_eq_lift_cardinalMk_field_pow_lift_rank`
`cardinal_lt_aleph0_of_finiteDimensional` 📖	mathematical	—	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder` `Cardinal.aleph0`	—	`Cardinal.lift_lt_aleph0` `lift_cardinalMk_eq_lift_cardinalMk_field_pow_lift_rank` `Cardinal.power_lt_aleph0` `Cardinal.lt_aleph0_of_finite` `Module.rank_lt_aleph0`
`finrank_eq_one_iff` 📖	mathematical	—	`Module.finrank` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Module.Basis`	—	`Fintype.card_unique` `Module.finrank_eq_card_basis`
`finrank_eq_one_iff'` 📖	mathematical	—	`Module.finrank` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`rank_eq_one_iff` `Cardinal.toNat_eq_iff` `one_ne_zero`
`finrank_le_one_iff` 📖	mathematical	—	`Module.finrank` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`rank_le_one_iff` `Module.finrank_eq_rank` `Nat.cast_le_one` `Cardinal.addLeftMono` `IsOrderedRing.toZeroLEOneClass` `Cardinal.isOrderedRing` `Cardinal.instCharZero`
`le_rank_iff_exists_linearIndependent` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `Module.rank` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Set.Elem` `LinearIndepOn`	—	`Module.Free.exists_basis` `Set.ext` `Module.Basis.reindexRange_apply` `LinearIndependent.linearIndepOn_id` `Module.Basis.linearIndependent` `Cardinal.le_mk_iff_exists_subset` `Module.Basis.mk_eq_rank''` `LinearIndepOn.mono` `LinearIndependent.cardinal_le_rank` `nontrivial_of_invariantBasisNumber` `invariantBasisNumber_of_rankCondition` `rankCondition_of_strongRankCondition`
`le_rank_iff_exists_linearIndependent_finset` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `Cardinal.instNatCast` `Module.rank` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Finset.card` `LinearIndependent` `Set` `Set.instMembership` `SetLike.coe` `Finset` `Finset.instSetLike`	—	—
`lift_cardinalMk_eq_lift_cardinalMk_field_pow_lift_rank` 📖	mathematical	—	`Cardinal.lift` `Cardinal` `Cardinal.instPowCardinal` `Module.rank` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid`	—	`Module.Free.exists_basis` `Cardinal.lift_mk_eq'` `RingHomInvPair.ids` `Cardinal.lift_umax` `Cardinal.lift_lift` `Cardinal.lift_power` `Module.Basis.mk_eq_rank''` `Cardinal.mk_arrow` `Equiv.cardinal_eq` `basis_finite_of_finite_spans` `nontrivial_of_invariantBasisNumber` `invariantBasisNumber_of_rankCondition` `rankCondition_of_strongRankCondition` `Finset.finite_toSet`
`rank_eq_one_iff` 📖	mathematical	—	`Module.rank` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Cardinal` `Cardinal.instOne` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`rank_le_one_iff` `Eq.le` `one_ne_zero` `NeZero.charZero_one` `Cardinal.instCharZero` `rank_subsingleton'` `nontrivial_of_invariantBasisNumber` `invariantBasisNumber_of_rankCondition` `rankCondition_of_strongRankCondition` `Nontrivial.to_nonempty` `smul_zero` `LE.le.antisymm` `Module.Free.exists_basis` `Equiv.subsingleton` `RingHomInvPair.ids` `Unique.instSubsingleton` `Cardinal.mk_eq_zero_iff` `Module.Basis.mk_eq_rank''` `Cardinal.lt_one_iff_zero` `not_le`
`rank_le_one_iff` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `Module.rank` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Cardinal.instOne` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`Module.Free.exists_basis` `isEmpty_or_nonempty` `Set.range_eq_empty` `Submodule.span_empty` `Module.Basis.span_eq` `smul_zero` `Zero.instNonempty` `Set.Subsingleton.eq_singleton_of_mem` `Set.subsingleton_range` `Cardinal.le_one_iff_subsingleton` `Module.Basis.mk_eq_rank''` `Set.mem_range_self` `Submodule.mem_top` `Submodule.mem_span_singleton` `Submodule.ext` `rank_top` `LE.le.trans_eq` `rank_span_le` `Cardinal.mk_fintype` `Fintype.card_unique` `Nat.cast_one`
`rank_submodule_eq_one_iff` 📖	mathematical	—	`Module.rank` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `Cardinal` `Cardinal.instOne` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Submodule.span` `Set` `Set.instSingletonSet`	—	`IsScalarTower.left` `Submodule.coe_smul` `AddSubmonoid.mk_eq_zero`
`rank_submodule_le_one_iff` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `Module.rank` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `Cardinal.instOne` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Submodule.span` `Set` `Set.instSingletonSet`	—	`SMulMemClass.smul_mem` `Submodule.smulMemClass`
`rank_submodule_le_one_iff'` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `Module.rank` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `Cardinal.instOne` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Submodule.span` `Set` `Set.instSingletonSet`	—	`rank_submodule_le_one_iff` `Module.Free.exists_basis` `Module.Basis.mk_eq_rank''` `Cardinal.mk_fintype` `Fintype.card_unique` `Nat.cast_one` `LE.le.trans` `LinearIndependent.cardinal_le_rank` `nontrivial_of_invariantBasisNumber` `invariantBasisNumber_of_rankCondition` `rankCondition_of_strongRankCondition` `LinearIndependent.map'` `Module.Basis.linearIndependent` `Submodule.ker_inclusion` `rank_span_le`

---

← Back to Index