Documentation Verification Report

Free

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

Statistics

Metric	Count
Definitions `ofFinrankEq`, `ofLiftRankEq`, `ofRankEq`, `smul_id_of_finrank_eq_one`, `basisUnique`, `finBasis`, `finBasisOfFinrankEq`	7
Theorems `instFiniteOfIsQuadraticExtension`, `nonempty_linearEquiv_iff_finrank_eq`, `nonempty_linearEquiv_of_finrank_eq`, `nonempty_equiv_iff_lift_rank_eq`, `nonempty_equiv_iff_rank_eq`, `smul_id_of_finrank_eq_one_apply`, `existsUnique_eq_smul_id_of_finrank_eq_one`, `nonempty_unique_index_of_finrank_eq_one`, `rank_eq_card_chooseBasisIndex`, `rank_eq_mk_of_infinite_lt`, `basisUnique_repr_eq_zero_iff`, `finite_iff_of_rank_eq_nsmul`, `finite_of_finrank_eq_succ`, `finite_of_finrank_pos`, `finrank_bot_le_finrank_of_isScalarTower_of_free`, `finrank_eq_card_chooseBasisIndex`, `finrank_mul_finrank`, `finrank_of_not_finite`, `finrank_top_le_finrank_of_isScalarTower_of_free`, `nonempty_linearEquiv_of_finrank_eq_one`, `rank_lt_aleph0_iff`, `subsingleton_of_rank_zero`, `lift_rank_mul_lift_rank`, `nonempty_linearEquiv_of_lift_rank_eq`, `nonempty_linearEquiv_of_rank_eq`, `rank_mul_rank`	26
Total	33

Algebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instFiniteOfIsQuadraticExtension` 📖	mathematical	—	`Module.Finite` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `toModule`	—	`Module.finite_of_finrank_eq_succ` `IsQuadraticExtension.toFree` `IsQuadraticExtension.finrank_eq_two`

FiniteDimensional

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nonempty_linearEquiv_iff_finrank_eq` 📖	mathematical	—	`LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Module.finrank`	—	`RingHomInvPair.ids` `LinearEquiv.finrank_eq` `nonempty_linearEquiv_of_finrank_eq`
`nonempty_linearEquiv_of_finrank_eq` 📖	mathematical	`Module.finrank`	`LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids`	—	`nonempty_linearEquiv_of_lift_rank_eq` `Cardinal.lift_natCast`

LinearEquiv

Definitions

Name	Category	Theorems
`ofFinrankEq` 📖	CompOp	—
`ofLiftRankEq` 📖	CompOp	—
`ofRankEq` 📖	CompOp	—
`smul_id_of_finrank_eq_one` 📖	CompOp	1 math math: `smul_id_of_finrank_eq_one_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nonempty_equiv_iff_lift_rank_eq` 📖	mathematical	—	`LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Cardinal.lift` `Module.rank`	—	`RingHomInvPair.ids` `lift_rank_eq` `nonempty_linearEquiv_of_lift_rank_eq`
`nonempty_equiv_iff_rank_eq` 📖	mathematical	—	`LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Module.rank`	—	`RingHomInvPair.ids` `rank_eq` `nonempty_linearEquiv_of_rank_eq`
`smul_id_of_finrank_eq_one_apply` 📖	mathematical	`Module.finrank` `CommSemiring.toSemiring`	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `LinearMap` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `LinearMap.addCommMonoid` `Semiring.toModule` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `EquivLike.toFunLike` `instEquivLike` `smul_id_of_finrank_eq_one` `LinearMap.instSMul` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `LinearMap.id`	—	`RingHomInvPair.ids` `smulCommClass_self`

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`existsUnique_eq_smul_id_of_finrank_eq_one` 📖	mathematical	`Module.finrank` `CommSemiring.toSemiring`	`ExistsUnique` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instSMul` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `id`	—	`RingHomInvPair.ids` `Module.nonempty_linearEquiv_of_finrank_eq_one` `smulCommClass_self` `ext` `mul_one` `LinearEquiv.apply_symm_apply` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `semilinearMapClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `LinearEquiv.symm_apply_apply` `LinearEquiv.congr_arg` `ext_iff`

Module

Definitions

Name	Category	Theorems
`basisUnique` 📖	CompOp	2 math math: `basisUnique_repr_eq_zero_iff`, `FiniteDimensional.basisSingleton_repr_apply`
`finBasis` 📖	CompOp	—
`finBasisOfFinrankEq` 📖	CompOp	1 math math: `AlternatingMap.measure_def`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`basisUnique_repr_eq_zero_iff` 📖	mathematical	`finrank`	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `Basis.repr` `basisUnique` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`RingHomInvPair.ids` `LinearEquiv.map_eq_zero_iff` `Finsupp.ext` `Unique.instSubsingleton` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `Finsupp.zero_apply`
`finite_iff_of_rank_eq_nsmul` 📖	mathematical	`rank` `Cardinal` `AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Cardinal.commSemiring`	`Finite`	—	`Cardinal.nsmul_lt_aleph0_iff_of_ne_zero`
`finite_of_finrank_eq_succ` 📖	mathematical	`finrank`	`Finite`	—	`finite_of_finrank_pos`
`finite_of_finrank_pos` 📖	mathematical	`finrank`	`Finite`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `finrank_of_not_finite`
`finrank_bot_le_finrank_of_isScalarTower_of_free` 📖	mathematical	—	`finrank` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`Finite.trans` `finrank_bot_le_finrank_of_isScalarTower` `finrank.eq_1` `Cardinal.toNat_eq_zero` `not_lt` `rank_lt_aleph0_iff` `zero_le` `Nat.instCanonicallyOrderedAdd`
`finrank_eq_card_chooseBasisIndex` 📖	mathematical	—	`finrank` `Fintype.card` `Free.ChooseBasisIndex` `Free.ChooseBasisIndex.fintype`	—	`Free.rank_eq_card_chooseBasisIndex` `Cardinal.mk_fintype` `Cardinal.toNat_natCast`
`finrank_mul_finrank` 📖	mathematical	—	`finrank` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`Cardinal.toNat_lift` `Cardinal.toNat_mul` `lift_rank_mul_lift_rank`
`finrank_of_not_finite` 📖	mathematical	`Finite`	`finrank`	—	`finrank.eq_1` `Cardinal.toNat_eq_zero` `not_lt` `rank_lt_aleph0_iff`
`finrank_top_le_finrank_of_isScalarTower_of_free` 📖	mathematical	—	`finrank`	—	`Finite.trans` `finrank_top_le_finrank_of_isScalarTower` `finrank.eq_1` `Cardinal.toNat_eq_zero` `not_lt` `rank_lt_aleph0_iff` `zero_le` `Nat.instCanonicallyOrderedAdd`
`nonempty_linearEquiv_of_finrank_eq_one` 📖	mathematical	`finrank`	`LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule`	—	`RingHomInvPair.ids` `Free.exists_basis` `Basis.nonempty_unique_index_of_finrank_eq_one` `RingHomCompTriple.ids` `Finite.of_fintype`
`rank_lt_aleph0_iff` 📖	mathematical	—	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder` `rank` `Cardinal.aleph0` `Finite`	—	`Free.rank_eq_card_chooseBasisIndex` `Cardinal.mk_lt_aleph0_iff` `Finite.of_basis` `Finite.of_fintype`
`subsingleton_of_rank_zero` 📖	—	`rank` `Cardinal` `Cardinal.instZero`	—	—	`Equiv.subsingleton` `RingHomInvPair.ids` `Unique.instSubsingleton` `Cardinal.mk_eq_zero_iff` `Basis.mk_eq_rank''`

Module.Basis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nonempty_unique_index_of_finrank_eq_one` 📖	mathematical	`Module.finrank`	`Unique`	—	`nontrivial_of_invariantBasisNumber` `invariantBasisNumber_of_rankCondition` `rankCondition_of_strongRankCondition` `Module.Finite.finite_basis` `Module.finite_of_finrank_pos` `Fintype.card_eq_one_iff_nonempty_unique` `Module.finrank_eq_card_basis`

Module.Free

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`rank_eq_card_chooseBasisIndex` 📖	mathematical	—	`Module.rank` `ChooseBasisIndex`	—	`Module.Basis.mk_eq_rank''`
`rank_eq_mk_of_infinite_lt` 📖	mathematical	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder` `Cardinal.lift`	`Module.rank`	—	`Cardinal.infinite_iff` `Cardinal.lift_le` `le_trans` `Cardinal.lift_aleph0` `LT.lt.le` `Cardinal.lift_mk_eq'` `RingHomInvPair.ids` `max_eq_iff` `Cardinal.mk_finsupp_lift_of_infinite'` `instNonemptyChooseBasisIndexOfNontrivial` `Infinite.instNontrivial` `Cardinal.lift_max` `Cardinal.lift_lift` `LT.lt.ne` `Cardinal.lift_umax`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lift_rank_mul_lift_rank` 📖	mathematical	—	`Cardinal` `Cardinal.instMul` `Cardinal.lift` `Module.rank` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`Cardinal.lift_id` `Module.Basis.mk_eq_rank` `Cardinal.lift_umax` `Cardinal.mk_prod` `Cardinal.lift_mul` `Cardinal.lift_lift`
`nonempty_linearEquiv_of_lift_rank_eq` 📖	mathematical	`Cardinal.lift` `Module.rank`	`LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids`	—	`RingHomInvPair.ids` `Module.Free.exists_basis` `Module.Basis.mk_eq_rank''` `Nonempty.map` `Cardinal.lift_mk_eq`
`nonempty_linearEquiv_of_rank_eq` 📖	mathematical	`Module.rank`	`LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids`	—	`nonempty_linearEquiv_of_lift_rank_eq`
`rank_mul_rank` 📖	mathematical	—	`Cardinal` `Cardinal.instMul` `Module.rank` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`Cardinal.lift_id` `lift_rank_mul_lift_rank`

---

← Back to Index