Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `basisSingleton`, `ofInjectiveEndo`, `ofInjectiveOfFinrankEq`, `basisOfFinrankZero`, `divisionRingOfFiniteDimensional`, `fieldOfFiniteDimensional`	6
Theorems `basisSingleton_apply`, `basisSingleton_repr_apply`, `exists_mul_eq_one`, `exists_relation_sum_zero_pos_coefficient_of_finrank_succ_lt_card`, `finiteDimensional_subalgebra`, `isUnit`, `of_rank_eq_nat`, `of_rank_eq_one`, `of_rank_eq_zero`, `of_subalgebra_toSubmodule`, `range_basisSingleton`, `subalgebra_toSubmodule`, `coe_ofInjectiveEndo`, `coe_ofInjectiveOfFinrankEq`, `ofInjectiveEndo_left_inv`, `ofInjectiveEndo_right_inv`, `lt_aleph0_of_finiteDimensional`, `comap_eq_sup_ker_of_disjoint`, `comp_eq_id_comm`, `finiteDimensional_of_surjective`, `finiteDimensional_range`, `injOn_iff_surjOn`, `injective_iff_surjective`, `instIsStablyFiniteRing`, `instIsStablyFiniteRingEnd`, `isUnit_iff_ker_eq_bot`, `isUnit_iff_range_eq_top`, `ker_comp_eq_of_commute_of_disjoint_ker`, `ker_eq_bot_iff_range_eq_top`, `ker_noncommProd_eq_of_supIndep_ker`, `mul_eq_one_comm`, `mul_eq_one_of_mul_eq_one`, `surjective_of_injective`, `injective_of_surjective`, `ker_pow_constant`, `finrank_mono`, `eq_of_le_of_finrank_eq`, `eq_of_le_of_finrank_le`, `finiteDimensional_toSubmodule`, `eq_of_le_of_finrank_eq`, `eq_of_le_of_finrank_le`, `eq_top_of_finrank_eq`, `finiteDimensional_finset_sup`, `finiteDimensional_iSup`, `finiteDimensional_inf_left`, `finiteDimensional_inf_right`, `finiteDimensional_of_le`, `finiteDimensional_sup`, `exists_smul_eq_of_finrank_eq_one`, `finiteDimensional_bot`, `finiteDimensional_finsupp`, `finrank_eq_one_iff_of_nonzero`, `finrank_eq_one_iff_of_nonzero'`, `finrank_span_singleton`, `finrank_zero_iff_forall_zero`, `surjective_of_nonzero_of_finrank_eq_one`	56
Total	62

FiniteDimensional

Definitions

Name	Category	Theorems
`basisSingleton` 📖	CompOp	3 math math: `basisSingleton_apply`, `basisSingleton_repr_apply`, `range_basisSingleton`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`basisSingleton_apply` 📖	mathematical	`Module.finrank` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid`	`DFunLike.coe` `Module.Basis` `Module.Basis.instFunLike` `basisSingleton`	—	`Unique.uniq` `Finsupp.single_eq_same` `one_smul`
`basisSingleton_repr_apply` 📖	mathematical	`Module.finrank` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid`	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `Module.Basis.repr` `basisSingleton` `Finsupp.single` `Unique.instInhabited` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Finsupp.instFunLike` `DFinsupp.instEquivLikeLinearEquiv` `Module.basisUnique` `Module.Free.of_divisionRing`	—	—
`exists_mul_eq_one` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`Algebra.to_smulCommClass` `LinearMap.injective_iff_surjective` `mul_right_inj'` `IsCancelMulZero.toIsLeftCancelMulZero` `IsDomain.toIsCancelMulZero`
`exists_relation_sum_zero_pos_coefficient_of_finrank_succ_lt_card` 📖	mathematical	`Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `Finset.card`	`Finset.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` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Finset` `Finset.instMembership` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Module.exists_nontrivial_relation_sum_zero_of_finrank_succ_lt_card` `IsNoetherianRing.strongRankCondition` `EuclideanDomain.toNontrivial` `PrincipalIdealRing.isNoetherianRing` `EuclideanDomain.to_principal_ideal_domain` `Finset.exists_pos_of_sum_zero_of_exists_nonzero` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid`
`finiteDimensional_subalgebra` 📖	mathematical	—	`FiniteDimensional` `Subalgebra` `Semifield.toCommSemiring` `Field.toSemifield` `Ring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Field.toDivisionRing` `Ring.toAddCommGroup` `Subalgebra.toRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Subalgebra.instModuleSubtypeMem`	—	`of_subalgebra_toSubmodule` `finiteDimensional_submodule`
`isUnit` 📖	mathematical	—	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring`	—	`Ne.isUnit`
`of_rank_eq_nat` 📖	mathematical	`Module.rank` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Cardinal` `Cardinal.instNatCast`	`FiniteDimensional`	—	`Module.finite_of_rank_eq_nat` `Module.Free.of_divisionRing`
`of_rank_eq_one` 📖	mathematical	`Module.rank` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Cardinal` `Cardinal.instOne`	`FiniteDimensional`	—	`Module.finite_of_rank_eq_one` `Module.Free.of_divisionRing`
`of_rank_eq_zero` 📖	mathematical	`Module.rank` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Cardinal` `Cardinal.instZero`	`FiniteDimensional`	—	`Module.finite_of_rank_eq_zero` `DivisionRing.isDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors`
`of_subalgebra_toSubmodule` 📖	mathematical	—	`FiniteDimensional` `Subalgebra` `Semifield.toCommSemiring` `Field.toSemifield` `Ring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Field.toDivisionRing` `Ring.toAddCommGroup` `Subalgebra.toRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Subalgebra.instModuleSubtypeMem`	—	`Subalgebra.finiteDimensional_toSubmodule`
`range_basisSingleton` 📖	mathematical	`Module.finrank` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid`	`Set.range` `DFunLike.coe` `Module.Basis` `Module.Basis.instFunLike` `basisSingleton` `Set` `Set.instSingletonSet`	—	`Set.range_unique` `basisSingleton_apply`
`subalgebra_toSubmodule` 📖	mathematical	—	`FiniteDimensional` `Submodule` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `Algebra.toModule` `SetLike.instMembership` `Submodule.setLike` `DFunLike.coe` `OrderEmbedding` `Subalgebra` `Preorder.toLE` `PartialOrder.toPreorder` `Subalgebra.instPartialOrder` `Submodule.instPartialOrder` `instFunLikeOrderEmbedding` `Subalgebra.toSubmodule` `Field.toDivisionRing` `Submodule.addCommGroup` `DivisionRing.toRing` `Ring.toAddCommGroup` `Submodule.module`	—	`Subalgebra.finiteDimensional_toSubmodule`

LinearEquiv

Definitions

Name	Category	Theorems
`ofInjectiveEndo` 📖	CompOp	3 math math: `coe_ofInjectiveEndo`, `ofInjectiveEndo_right_inv`, `ofInjectiveEndo_left_inv`
`ofInjectiveOfFinrankEq` 📖	CompOp	1 math math: `coe_ofInjectiveOfFinrankEq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_ofInjectiveEndo` 📖	mathematical	`DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike`	`LinearEquiv` `RingHomInvPair.ids` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `ofInjectiveEndo`	—	`RingHomInvPair.ids`
`coe_ofInjectiveOfFinrankEq` 📖	mathematical	`DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `Module.finrank`	`toLinearMap` `RingHomInvPair.ids` `ofInjectiveOfFinrankEq`	—	`RingHomInvPair.ids`
`ofInjectiveEndo_left_inv` 📖	mathematical	`DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike`	`Module.End.instMul` `toLinearMap` `RingHomInvPair.ids` `symm` `ofInjectiveEndo` `Module.End.instOne`	—	`LinearMap.ext` `RingHomInvPair.ids` `symm_apply_apply`
`ofInjectiveEndo_right_inv` 📖	mathematical	`DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike`	`Module.End.instMul` `toLinearMap` `RingHomInvPair.ids` `symm` `ofInjectiveEndo` `Module.End.instOne`	—	`LinearMap.ext` `RingHomInvPair.ids` `apply_symm_apply`

LinearIndependent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lt_aleph0_of_finiteDimensional` 📖	mathematical	`LinearIndependent` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid`	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder` `Cardinal.aleph0`	—	`lt_aleph0_of_finite` `IsNoetherianRing.strongRankCondition` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `PrincipalIdealRing.isNoetherianRing` `DivisionSemiring.isPrincipalIdealRing`

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap_eq_sup_ker_of_disjoint` 📖	mathematical	`Submodule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instFunLike` `Disjoint` `Submodule.instPartialOrder` `Submodule.instOrderBot` `ker`	`Submodule.comap` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice`	—	`le_antisymm` `surjective_of_injective` `injective_restrict_iff_disjoint` `Submodule.mem_sup` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `semilinearMapClass` `sub_self` `add_sub_cancel` `sup_le_iff` `ker_le_comap`
`comp_eq_id_comm` 📖	mathematical	—	`comp` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `id`	—	`mul_eq_one_comm` `instIsDedekindFiniteMonoidOfIsStablyFiniteRing` `instIsStablyFiniteRingEnd`
`finiteDimensional_of_surjective` 📖	mathematical	`range` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `Top.top` `Submodule` `Submodule.instTop`	`FiniteDimensional`	—	`RingHomSurjective.ids` `Module.Finite.of_surjective` `range_eq_top`
`finiteDimensional_range` 📖	mathematical	—	`FiniteDimensional` `Submodule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `Submodule.addCommGroup` `DivisionRing.toRing` `Submodule.module`	—	`Module.Finite.range`
`injOn_iff_surjOn` 📖	mathematical	`Submodule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instFunLike`	`Set.InjOn` `SetLike.coe` `Set.SurjOn`	—	`Set.injOn_iff_injective` `Set.MapsTo.restrict_surjective_iff`
`injective_iff_surjective` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike`	—	`surjective_of_injective` `RingHomCompTriple.ids` `exists_rightInverse_of_surjective` `Module.Projective.of_free` `Module.Free.of_divisionRing` `RingHomSurjective.ids` `range_eq_top` `ext_iff` `Function.RightInverse.injective`
`instIsStablyFiniteRing` 📖	mathematical	—	`IsStablyFiniteRing` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DivisionRing.toRing`	—	`isStablyFiniteRing_iff_isDedekindFiniteMonoid_moduleEnd` `RingHomCompTriple.ids` `exists_rightInverse_of_surjective` `Module.Projective.of_free` `Module.Free.function` `Finite.of_fintype` `Module.Free.self` `RingHomSurjective.ids` `range_eq_top` `injective_iff_surjective` `FiniteDimensional.finiteDimensional_pi'` `FiniteDimensional.finiteDimensional_self` `mul_one` `one_mul` `mul_assoc`
`instIsStablyFiniteRingEnd` 📖	mathematical	—	`IsStablyFiniteRing` `Module.End` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Module.End.instSemiring` `addCommMonoid` `RingHom.id`	—	`RingHomInvPair.ids` `RingHomCompTriple.ids` `Finite.of_fintype` `RingEquiv.isStablyFiniteRing_iff` `RingEquiv.instRingEquivClass` `instIsStablyFiniteRingEndForallOfFinite`
`isUnit_iff_ker_eq_bot` 📖	mathematical	—	`IsUnit` `LinearMap` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Module.End.instMonoid` `ker` `Bot.bot` `Submodule` `Submodule.instBot`	—	`ker_eq_bot_of_inverse` `RingHomInvPair.ids` `Units.inv_mul` `ker_eq_bot` `LinearEquiv.ofInjectiveEndo_right_inv` `LinearEquiv.ofInjectiveEndo_left_inv`
`isUnit_iff_range_eq_top` 📖	mathematical	—	`IsUnit` `LinearMap` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Module.End.instMonoid` `range` `RingHomSurjective.ids` `Top.top` `Submodule` `Submodule.instTop`	—	`RingHomSurjective.ids` `isUnit_iff_ker_eq_bot` `ker_eq_bot_iff_range_eq_top`
`ker_comp_eq_of_commute_of_disjoint_ker` 📖	mathematical	`Commute` `LinearMap` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Module.End.instMul` `Disjoint` `Submodule` `Submodule.instPartialOrder` `Submodule.instOrderBot` `ker`	`comp` `RingHomCompTriple.ids` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice`	—	`RingHomCompTriple.ids` `comp_apply` `Module.End.mul_eq_comp` `Commute.eq` `Module.End.mul_apply` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `semilinearMapClass` `ker_comp` `comap_eq_sup_ker_of_disjoint` `FiniteDimensional.finiteDimensional_submodule`
`ker_eq_bot_iff_range_eq_top` 📖	mathematical	—	`ker` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `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`
`ker_noncommProd_eq_of_supIndep_ker` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `Finset.instSetLike` `Function.onFun` `LinearMap` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Module.End.instMonoid` `Finset.SupIndep` `Submodule` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `Submodule.instOrderBot` `ker`	`Finset.noncommProd` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Finset.instMembership`	—	`Finset.induction_on` `iSup_congr_Prop` `iSup_neg` `iSup_bot` `Set.Pairwise.mono` `Finset.subset_insert` `Finset.SupIndep.subset` `Finset.mem_insert_of_mem` `Finset.noncommProd_insert_of_notMem` `RingHomCompTriple.ids` `Module.End.mul_eq_comp` `ker_comp_eq_of_commute_of_disjoint_ker` `Finset.noncommProd_commute` `Finset.mem_insert_self` `Finset.supIndep_iff_disjoint_erase` `Finset.erase_insert_eq_erase` `Finset.erase_eq_of_notMem` `Finset.sup_eq_iSup` `iSup_insert`
`mul_eq_one_comm` 📖	mathematical	—	`LinearMap` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Module.End.instMul` `Module.End.instOne`	—	`mul_eq_one_comm` `instIsDedekindFiniteMonoidOfIsStablyFiniteRing` `instIsStablyFiniteRingEnd` `Module.Free.of_divisionRing` `instIsStablyFiniteRing`
`mul_eq_one_of_mul_eq_one` 📖	—	`LinearMap` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Module.End.instMul` `Module.End.instOne`	—	—	`IsDedekindFiniteMonoid.mul_eq_one_symm` `instIsDedekindFiniteMonoidOfIsStablyFiniteRing` `instIsStablyFiniteRingEnd` `Module.Free.of_divisionRing` `instIsStablyFiniteRing`
`surjective_of_injective` 📖	—	`DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike`	—	—	`RingHomSurjective.ids` `rank_range_of_injective` `range_eq_top` `Submodule.eq_top_of_finrank_eq` `Cardinal.instCharZero` `Module.finrank_eq_rank` `IsNoetherianRing.strongRankCondition` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `PrincipalIdealRing.isNoetherianRing` `DivisionSemiring.isPrincipalIdealRing` `Module.Finite.range`

Module.End

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`injective_of_surjective` 📖	—	`DFunLike.coe` `Module.End` `LinearMap.instFunLike` `RingHom.id` `Semiring.toNonAssocSemiring`	—	—	`RingHomCompTriple.ids` `Module.projective_lifting_property` `Module.Projective.of_free` `LinearMap.injective_of_comp_eq_id` `RingHomInvPair.ids` `IsDedekindFiniteMonoid.mul_eq_one_symm` `instIsDedekindFiniteMonoidOfIsStablyFiniteRing` `LinearMap.instIsStablyFiniteRingEnd`
`ker_pow_constant` 📖	—	`LinearMap.ker` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `Module.End` `Monoid.toNatPow` `instMonoid`	—	—	`add_zero` `le_antisymm` `add_comm` `pow_add` `LinearMap.ker_le_ker_comp` `add_assoc` `RingHomCompTriple.ids` `mul_eq_comp` `LinearMap.ker_comp` `le_refl`

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finrank_mono` 📖	mathematical	`Set` `instHasSubset`	`finrank` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid`	—	`Submodule.finrank_mono` `IsNoetherianRing.strongRankCondition` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `PrincipalIdealRing.isNoetherianRing` `DivisionSemiring.isPrincipalIdealRing` `FiniteDimensional.finiteDimensional_submodule` `Submodule.span_mono`

Subalgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_of_le_of_finrank_eq` 📖	—	`Subalgebra` `Semifield.toCommSemiring` `Field.toSemifield` `Ring.toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Module.finrank` `SetLike.instMembership` `instSetLike` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `toRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instModuleSubtypeMem`	—	—	`eq_of_le_of_finrank_le` `Eq.ge`
`eq_of_le_of_finrank_le` 📖	—	`Subalgebra` `Semifield.toCommSemiring` `Field.toSemifield` `Ring.toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Module.finrank` `SetLike.instMembership` `instSetLike` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `toRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instModuleSubtypeMem`	—	—	`toSubmodule_injective` `Submodule.eq_of_le_of_finrank_le`
`finiteDimensional_toSubmodule` 📖	mathematical	—	`FiniteDimensional` `Submodule` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `Algebra.toModule` `SetLike.instMembership` `Submodule.setLike` `DFunLike.coe` `OrderEmbedding` `Subalgebra` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Submodule.instPartialOrder` `instFunLikeOrderEmbedding` `toSubmodule` `Field.toDivisionRing` `Submodule.addCommGroup` `DivisionRing.toRing` `Ring.toAddCommGroup` `Submodule.module` `instSetLike` `toRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instModuleSubtypeMem`	—	—

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_of_le_of_finrank_eq` 📖	—	`Submodule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Module.finrank` `SetLike.instMembership` `setLike` `addCommMonoid` `module`	—	—	`eq_of_le_of_finrank_le` `Eq.ge`
`eq_of_le_of_finrank_le` 📖	—	`Submodule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Module.finrank` `SetLike.instMembership` `setLike` `addCommMonoid` `module`	—	—	`le_antisymm` `comap_subtype_eq_top` `eq_top_of_finrank_eq` `finrank_le` `IsNoetherianRing.strongRankCondition` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `PrincipalIdealRing.isNoetherianRing` `DivisionSemiring.isPrincipalIdealRing` `LinearEquiv.finrank_eq`
`eq_top_of_finrank_eq` 📖	mathematical	`Module.finrank` `Submodule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `addCommMonoid` `module`	`Top.top` `instTop`	—	`Set.image_congr` `Module.Basis.coe_ofVectorSpace` `Subtype.range_coe_subtype` `LinearIndepOn.image` `LinearIndependent.linearIndepOn_id` `Module.Basis.linearIndependent` `Module.Basis.span_eq` `ker_subtype` `Set.subset_univ` `Set.eq_of_subset_of_card_le` `LinearIndependent.set_finite_of_isNoetherian` `isNoetherian_of_isNoetherianRing_of_finite` `PrincipalIdealRing.isNoetherianRing` `DivisionSemiring.isPrincipalIdealRing` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `FiniteDimensional.finiteDimensional_submodule` `LinearIndepOn.subset_extend` `Set.card_image_of_injective` `Subtype.coe_injective` `Module.finrank_eq_card_basis` `IsNoetherianRing.strongRankCondition` `le_refl` `Module.Basis.coe_extend` `Subtype.range_coe` `coe_subtype` `RingHomSurjective.ids` `span_image` `map_top` `range_subtype`
`finiteDimensional_finset_sup` 📖	mathematical	`FiniteDimensional` `Submodule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `addCommGroup` `DivisionRing.toRing` `module`	`Finset.sup` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice` `instOrderBot`	—	`finite_finset_sup`
`finiteDimensional_iSup` 📖	mathematical	`FiniteDimensional` `Submodule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `addCommGroup` `DivisionRing.toRing` `module`	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice`	—	`finite_iSup`
`finiteDimensional_inf_left` 📖	mathematical	—	`FiniteDimensional` `Submodule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `instMin` `addCommGroup` `DivisionRing.toRing` `module`	—	`finiteDimensional_of_le` `inf_le_left`
`finiteDimensional_inf_right` 📖	mathematical	—	`FiniteDimensional` `Submodule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `instMin` `addCommGroup` `DivisionRing.toRing` `module`	—	`finiteDimensional_of_le` `inf_le_right`
`finiteDimensional_of_le` 📖	mathematical	`Submodule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`FiniteDimensional` `SetLike.instMembership` `setLike` `addCommGroup` `DivisionRing.toRing` `module`	—	`Module.IsNoetherian.finite` `isNoetherian_of_le` `isNoetherian_of_isNoetherianRing_of_finite` `PrincipalIdealRing.isNoetherianRing` `DivisionSemiring.isPrincipalIdealRing`
`finiteDimensional_sup` 📖	mathematical	—	`FiniteDimensional` `Submodule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice` `addCommGroup` `DivisionRing.toRing` `module`	—	`finite_sup`

(root)

Definitions

Name	Category	Theorems
`basisOfFinrankZero` 📖	CompOp	—
`divisionRingOfFiniteDimensional` 📖	CompOp	—
`fieldOfFiniteDimensional` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_smul_eq_of_finrank_eq_one` 📖	mathematical	`Module.finrank` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `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`	—	`FiniteDimensional.of_finrank_eq_succ` `Submodule.eq_top_of_finrank_eq` `finrank_span_singleton` `Submodule.mem_top` `Submodule.mem_span_singleton`
`finiteDimensional_bot` 📖	mathematical	—	`FiniteDimensional` `Submodule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Bot.bot` `Submodule.instBot` `Submodule.addCommGroup` `DivisionRing.toRing` `Submodule.module`	—	`FiniteDimensional.of_rank_eq_zero` `rank_subsingleton'` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `Unique.instSubsingleton`
`finiteDimensional_finsupp` 📖	mathematical	—	`FiniteDimensional` `Finsupp` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Finsupp.instAddCommGroup` `Finsupp.module` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid`	—	`Module.Finite.finsupp`
`finrank_eq_one_iff_of_nonzero` 📖	mathematical	—	`Module.finrank` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.span` `Set` `Set.instSingletonSet` `Top.top` `Submodule` `Submodule.instTop`	—	`FiniteDimensional.range_basisSingleton` `Module.Basis.span_eq` `Module.finrank_eq_card_basis` `IsNoetherianRing.strongRankCondition` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `PrincipalIdealRing.isNoetherianRing` `DivisionSemiring.isPrincipalIdealRing` `LinearIndependent.of_subsingleton` `DivisionRing.isDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `Matrix.range_cons` `Matrix.range_empty` `Set.union_empty`
`finrank_eq_one_iff_of_nonzero'` 📖	mathematical	—	`Module.finrank` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `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`	—	`finrank_eq_one_iff_of_nonzero` `Submodule.span_singleton_eq_top_iff`
`finrank_span_singleton` 📖	mathematical	—	`Module.finrank` `Submodule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set` `Set.instSingletonSet` `Submodule.addCommMonoid` `Submodule.module`	—	`le_antisymm` `finrank_span_le_card` `IsNoetherianRing.strongRankCondition` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `PrincipalIdealRing.isNoetherianRing` `DivisionSemiring.isPrincipalIdealRing` `Module.finrank_pos_iff` `FiniteDimensional.span_singleton` `DivisionRing.isDomain` `Ideal.instIsTorsionFreeSubtypeMemSubmodule` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `Submodule.mem_span_singleton_self` `Subtype.coe_ne_coe`
`finrank_zero_iff_forall_zero` 📖	mathematical	—	`Module.finrank` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`Module.finrank_zero_iff` `IsNoetherianRing.strongRankCondition` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `PrincipalIdealRing.isNoetherianRing` `DivisionSemiring.isPrincipalIdealRing` `DivisionRing.isDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors`
`surjective_of_nonzero_of_finrank_eq_one` 📖	mathematical	`Module.finrank` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid`	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	—	`DFunLike.ne_iff` `finrank_eq_one_iff_of_nonzero'` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass`

---

← Back to Index