Constructions

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

Statistics

Metric	Count
Definitions `sumQuot`, `finrank`, `finDimVectorspaceEquiv`	3
Theorems `quotient_iff_union`, `union_id_of_quotient`, `union_of_quotient`, `sumElim_of_quotient`, `sumQuot_inl`, `sumQuot_inr`, `sumQuot_repr_inl`, `sumQuot_repr_inl_of_mem`, `sumQuot_repr_inr`, `sumQuot_repr_inr_of_mem`, `sumQuot_repr_left`, `finrank_baseChange`, `finrank_directSum`, `finrank_fin_fun`, `finrank_finsupp`, `finrank_finsupp_self`, `finrank_fintype_fun_eq_card`, `finrank_matrix`, `finrank_pi`, `finrank_pi_fintype`, `finrank_prod`, `finrank_tensorProduct`, `rank_baseChange`, `dim_spanSubset`, `finrank_bot`, `finrank_toSubmodule`, `rank_bot`, `rank_toSubmodule`, `rank_top`, `finrank_le`, `finrank_map_le`, `finrank_mono`, `finrank_quotient_le`, `lt_of_le_of_finrank_lt_finrank`, `lt_top_of_finrank_lt_finrank`, `finrank_le_of_span_eq_top`, `finrank_range_le_card`, `finrank_span_eq_card`, `finrank_span_finset_eq_card`, `finrank_span_finset_le_card`, `finrank_span_le_card`, `finrank_span_set_eq_card`, `finrank_ulift`, `lift_rank_add_lift_rank_le_rank_prod`, `linearIndepOn_union_iff_quotient`, `rank_add_rank_le_rank_prod`, `rank_directSum`, `rank_fin_fun`, `rank_finsupp`, `rank_finsupp'`, `rank_finsupp_self`, `rank_finsupp_self'`, `rank_fun`, `rank_fun'`, `rank_fun_eq_lift_mul`, `rank_matrix`, `rank_matrix'`, `rank_matrix''`, `rank_matrix_module`, `rank_matrix_module'`, `rank_pi`, `rank_prod`, `rank_prod'`, `rank_quotient_add_rank_le`, `rank_quotient_le`, `rank_span_finset_le`, `rank_span_le`, `rank_span_of_finset`, `rank_tensorProduct`, `rank_tensorProduct'`, `rank_ulift`, `span_lt_of_subset_of_card_lt_finrank`, `span_lt_top_of_card_lt_finrank`, `subalgebra_top_finrank_eq_submodule_top_finrank`, `subalgebra_top_rank_eq_submodule_top_rank`	75
Total	78

LinearIndepOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`quotient_iff_union` 📖	mathematical	`LinearIndepOn` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	`LinearIndepOn` `HasQuotient.Quotient` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.hasQuotient` `Submodule.span` `Set.image` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `LinearMap.instFunLike` `Submodule.mkQ` `Set` `Set.instUnion`	—	`linearIndepOn_union_iff_quotient`
`union_id_of_quotient` 📖	mathematical	`Set` `Set.instHasSubset` `SetLike.coe` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.setLike` `LinearIndepOn` `HasQuotient.Quotient` `Submodule.hasQuotient` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `LinearMap.instFunLike` `Submodule.mkQ`	`LinearIndepOn` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Set` `Set.instUnion`	—	`union_of_quotient` `Set.image_id` `of_comp` `Submodule.span_le`
`union_of_quotient` 📖	mathematical	`LinearIndepOn` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `HasQuotient.Quotient` `Submodule` `Submodule.hasQuotient` `Submodule.span` `Set.image` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `LinearMap.instFunLike` `Submodule.mkQ`	`LinearIndepOn` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Set` `Set.instUnion`	—	`union` `of_comp` `Submodule.ker_mkQ` `Set.ext` `Disjoint.symm` `Submodule.range_ker_disjoint`

LinearIndependent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sumElim_of_quotient` 📖	mathematical	`LinearIndependent` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `HasQuotient.Quotient` `Submodule.hasQuotient` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module`	`LinearIndependent` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike`	—	`sum_type` `map'` `Submodule.ker_subtype` `of_comp` `Submodule.disjoint_def` `Submodule.span_le` `Set.range_subset_iff` `Subtype.prop` `Finsupp.mem_span_range_iff_exists_finsupp` `linearIndependent_iff` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass` `map_finsuppSum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `Finsupp.sum_zero_index`

Module

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finrank_baseChange` 📖	mathematical	—	`finrank` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `CommSemiring.toSemiring`	—	`Algebra.to_smulCommClass` `IsScalarTower.to_smulCommClass` `IsScalarTower.right` `finrank_tensorProduct` `Free.self` `finrank_self` `one_mul`
`finrank_directSum` 📖	mathematical	`Free` `Finite`	`finrank` `DirectSum` `instAddCommMonoidDirectSum` `DirectSum.instModule` `Finset.sum` `Nat.instAddCommMonoid` `Finset.univ`	—	`rank_directSum` `Free.rank_eq_card_chooseBasisIndex` `Cardinal.mk_toNat_eq_card` `Fintype.card_sigma` `Finset.sum_congr`
`finrank_fin_fun` 📖	mathematical	—	`finrank` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Pi.Function.module` `Semiring.toModule`	—	`finrank_fintype_fun_eq_card` `Fintype.card_fin`
`finrank_finsupp` 📖	mathematical	—	`finrank` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finsupp.instAddCommMonoid` `Finsupp.module` `Fintype.card`	—	`finrank.eq_1` `rank_finsupp` `Cardinal.mk_toNat_eq_card` `Cardinal.toNat_mul` `Cardinal.toNat_lift`
`finrank_finsupp_self` 📖	mathematical	—	`finrank` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `Fintype.card`	—	`finrank.eq_1` `rank_finsupp_self` `Cardinal.mk_toNat_eq_card` `Cardinal.toNat_lift`
`finrank_fintype_fun_eq_card` 📖	mathematical	—	`finrank` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Pi.Function.module` `Semiring.toModule` `Fintype.card`	—	`finrank_eq_of_rank_eq` `rank_fun'`
`finrank_matrix` 📖	mathematical	—	`finrank` `Matrix` `Matrix.addCommMonoid` `Matrix.module` `Fintype.card`	—	`rank_matrix_module` `Finite.of_fintype` `Cardinal.mk_fintype` `Cardinal.lift_natCast` `map_mul` `MonoidHomClass.toMulHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass` `Cardinal.toNat_natCast` `Cardinal.toNat_lift`
`finrank_pi` 📖	mathematical	—	`finrank` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Pi.Function.module` `Semiring.toModule` `Fintype.card`	—	`rank_pi` `Free.self` `Finite.of_fintype` `rank_self` `Cardinal.sum_const` `Cardinal.mk_fintype` `Cardinal.lift_natCast` `Cardinal.lift_one` `mul_one` `Cardinal.toNat_natCast`
`finrank_pi_fintype` 📖	mathematical	`Free` `Finite`	`finrank` `Pi.addCommMonoid` `Pi.module` `Finset.sum` `Nat.instAddCommMonoid` `Finset.univ`	—	`rank_pi` `Finite.of_fintype` `Free.rank_eq_card_chooseBasisIndex` `Cardinal.mk_toNat_eq_card` `Fintype.card_sigma` `Finset.sum_congr`
`finrank_prod` 📖	mathematical	—	`finrank` `Prod.instAddCommMonoid` `Prod.instModule`	—	`rank_prod` `Cardinal.toNat_add` `rank_lt_aleph0` `Cardinal.toNat_lift`
`finrank_tensorProduct` 📖	mathematical	—	`finrank` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `IsScalarTower.to_smulCommClass` `CommSemiring.toSemiring`	—	`IsScalarTower.to_smulCommClass` `rank_tensorProduct` `map_mul` `MonoidHomClass.toMulHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass` `Cardinal.toNat_lift`
`rank_baseChange` 📖	mathematical	—	`rank` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `Cardinal.lift` `CommSemiring.toSemiring`	—	`Algebra.to_smulCommClass` `IsScalarTower.to_smulCommClass` `IsScalarTower.right` `rank_tensorProduct` `Free.self` `rank_self` `Cardinal.lift_one` `one_mul`

Module.Basis

Definitions

Name	Category	Theorems
`sumQuot` 📖	CompOp	7 math math: `sumQuot_repr_left`, `sumQuot_repr_inl`, `sumQuot_repr_inl_of_mem`, `sumQuot_repr_inr_of_mem`, `sumQuot_inr`, `sumQuot_inl`, `sumQuot_repr_inr`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sumQuot_inl` 📖	mathematical	—	`DFunLike.coe` `Module.Basis` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike` `sumQuot` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module`	—	—
`sumQuot_inr` 📖	mathematical	—	`CommRing.toRing` `DFunLike.coe` `Module.Basis` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike` `sumQuot` `HasQuotient.Quotient` `Submodule` `Submodule.hasQuotient` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module`	—	`Function.rightInverse_surjInv` `Submodule.mkQ_surjective`
`sumQuot_repr_inl` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Finsupp.instFunLike` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `repr` `sumQuot` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module`	—	`RingHomInvPair.ids` `repr_apply_eq` `map_add` `SemilinearMapClass.toAddHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass` `sumQuot_repr_left` `Finsupp.single_apply`
`sumQuot_repr_inl_of_mem` 📖	mathematical	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike`	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Finsupp.instFunLike` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `repr` `sumQuot` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module`	—	`sumQuot_repr_inl`
`sumQuot_repr_inr` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Finsupp.instFunLike` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `repr` `sumQuot` `HasQuotient.Quotient` `Submodule` `Submodule.hasQuotient` `CommRing.toRing` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `LinearMap` `Ring.toSemiring` `LinearMap.instFunLike` `Submodule.mkQ`	—	`RingHomInvPair.ids` `RingHomCompTriple.ids` `LinearMap.comp_apply` `LinearMap.ext_iff` `ext` `sumQuot_inl` `sumQuot_repr_left` `Finsupp.single_eq_of_ne` `Submodule.Quotient.mk_eq_zero` `Submodule.coe_mem` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `repr_self` `Finsupp.single_apply` `sumQuot_inr`
`sumQuot_repr_inr_of_mem` 📖	mathematical	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike`	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Finsupp.instFunLike` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `repr` `sumQuot` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`RingHomInvPair.ids` `sumQuot_repr_inr` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass`
`sumQuot_repr_left` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `repr` `sumQuot` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Module.Basis` `Submodule.addCommMonoid` `Submodule.module` `instFunLike` `Finsupp.single` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`RingHomInvPair.ids` `apply_eq_iff` `sumQuot_inl`

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dim_spanSubset` 📖	mathematical	—	`Module.finrank` `Submodule` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Function.module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `spanSubset` `Submodule.addCommMonoid` `Submodule.module` `Set.ncard`	—	`spanSubset.eq_1` `finrank_span_set_eq_card` `LinearIndepOn.id_image` `Module.Basis.linearIndepOn` `Set.toFinset_card` `Fintype.card_eq_nat_card` `Nat.card_coe_set_eq` `Set.ncard_image_of_injective` `Module.Basis.injective`

Set

Definitions

Name	Category	Theorems
`finrank` 📖	CompOp	7 math math: `linearIndependent_iff_card_le_finrank_span`, `Real.finrank_eq_int_finrank_of_discrete`, `finrank_empty`, `finrank_range_le_card`, `finrank_span_finset_le_card`, `finrank_mono`, `linearIndependent_iff_card_eq_finrank_span`

Subalgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finrank_bot` 📖	mathematical	—	`Module.finrank` `Subalgebra` `CommRing.toCommSemiring` `Ring.toSemiring` `SetLike.instMembership` `instSetLike` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `toRing` `instModuleSubtypeMem`	—	`Module.finrank_eq_of_rank_eq` `rank_bot` `Nat.cast_one`
`finrank_toSubmodule` 📖	mathematical	—	`Module.finrank` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `SetLike.instMembership` `Submodule.setLike` `DFunLike.coe` `OrderEmbedding` `Subalgebra` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Submodule.instPartialOrder` `instFunLikeOrderEmbedding` `toSubmodule` `Submodule.addCommMonoid` `Submodule.module` `instSetLike` `toSemiring` `instModuleSubtypeMem`	—	—
`rank_bot` 📖	mathematical	—	`Module.rank` `Subalgebra` `CommRing.toCommSemiring` `Ring.toSemiring` `SetLike.instMembership` `instSetLike` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `toRing` `instModuleSubtypeMem` `Cardinal` `Cardinal.instOne`	—	`LinearEquiv.rank_eq` `RingHomInvPair.ids` `Algebra.toSubmodule_bot` `Submodule.one_eq_span` `rank_span_set` `Module.nontrivial` `LinearIndepOn.singleton` `one_ne_zero` `NeZero.one` `Cardinal.mk_singleton`
`rank_toSubmodule` 📖	mathematical	—	`Module.rank` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `SetLike.instMembership` `Submodule.setLike` `DFunLike.coe` `OrderEmbedding` `Subalgebra` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Submodule.instPartialOrder` `instFunLikeOrderEmbedding` `toSubmodule` `Submodule.addCommMonoid` `Submodule.module` `instSetLike` `toSemiring` `instModuleSubtypeMem`	—	—
`rank_top` 📖	mathematical	—	`Module.rank` `Subalgebra` `SetLike.instMembership` `instSetLike` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `toSemiring` `instModuleSubtypeMem` `Algebra.toModule`	—	`subalgebra_top_rank_eq_submodule_top_rank` `rank_top`

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finrank_le` 📖	mathematical	—	`Module.finrank` `Submodule` `SetLike.instMembership` `setLike` `addCommMonoid` `module`	—	`Cardinal.toNat_le_toNat` `rank_le` `Module.rank_lt_aleph0`
`finrank_map_le` 📖	mathematical	—	`Module.finrank` `Submodule` `SetLike.instMembership` `setLike` `map` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `addCommMonoid` `module`	—	`Module.finrank_le_finrank_of_rank_le_rank` `RingHomSurjective.ids` `lift_rank_map_le` `Module.rank_lt_aleph0`
`finrank_mono` 📖	mathematical	`Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`Module.finrank` `Submodule` `SetLike.instMembership` `setLike` `addCommMonoid` `module`	—	`Cardinal.toNat_le_toNat` `rank_mono` `Module.rank_lt_aleph0`
`finrank_quotient_le` 📖	mathematical	—	`Module.finrank` `HasQuotient.Quotient` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `hasQuotient` `Quotient.addCommGroup` `Quotient.module`	—	`Cardinal.toNat_le_toNat` `LinearMap.rank_le_of_surjective` `Quot.mk_surjective` `Module.rank_lt_aleph0`
`lt_of_le_of_finrank_lt_finrank` 📖	mathematical	`Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Module.finrank` `SetLike.instMembership` `setLike` `addCommMonoid` `module`	`Submodule` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder`	—	`lt_of_le_of_ne` `ne_of_lt`
`lt_top_of_finrank_lt_finrank` 📖	mathematical	`Module.finrank` `Submodule` `SetLike.instMembership` `setLike` `addCommMonoid` `module`	`Submodule` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `Top.top` `instTop`	—	`lt_of_le_of_finrank_lt_finrank` `le_top` `finrank_top`

(root)

Definitions

Name	Category	Theorems
`finDimVectorspaceEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finrank_le_of_span_eq_top` 📖	mathematical	`Submodule.span` `Set.range` `Top.top` `Submodule` `Submodule.instTop`	`Module.finrank` `Fintype.card`	—	`finrank_top` `LE.le.trans` `finrank_span_le_card` `Set.toFinset_card` `Fintype.card_range_le`
`finrank_range_le_card` 📖	mathematical	—	`Set.finrank` `Set.range` `Fintype.card`	—	`LE.le.trans` `finrank_span_le_card` `Set.toFinset_range` `Finset.card_image_le`
`finrank_span_eq_card` 📖	mathematical	`LinearIndependent`	`Module.finrank` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.range` `Submodule.addCommMonoid` `Submodule.module` `Fintype.card`	—	`Module.finrank_eq_of_rank_eq` `rank_span` `Cardinal.lift_eq_nat_iff` `Cardinal.lift_natCast` `Cardinal.mk_fintype` `Cardinal.mk_range_eq_of_injective` `LinearIndependent.injective`
`finrank_span_finset_eq_card` 📖	mathematical	`LinearIndepOn` `SetLike.coe` `Finset` `Finset.instSetLike`	`Module.finrank` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `SetLike.coe` `Finset` `Finset.instSetLike` `Submodule.addCommMonoid` `Submodule.module` `Finset.card`	—	`Finset.ext` `Finset.toFinset_coe` `finrank_span_set_eq_card`
`finrank_span_finset_le_card` 📖	mathematical	—	`Set.finrank` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.card`	—	`finrank_span_le_card` `Finset.toFinset_coe`
`finrank_span_le_card` 📖	mathematical	—	`Module.finrank` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Submodule.addCommMonoid` `Submodule.module` `Finset.card` `Set.toFinset`	—	`Module.finrank_le_of_rank_le` `Set.toFinset_card` `Cardinal.mk_fintype` `rank_span_le`
`finrank_span_set_eq_card` 📖	mathematical	`LinearIndepOn`	`Module.finrank` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Submodule.addCommMonoid` `Submodule.module` `Finset.card` `Set.toFinset`	—	`Module.finrank_eq_of_rank_eq` `rank_span_set` `Set.toFinset_card` `Cardinal.mk_fintype`
`finrank_ulift` 📖	mathematical	—	`Module.finrank` `ULift.addCommMonoid` `ULift.module'`	—	`rank_ulift` `Cardinal.toNat_lift`
`lift_rank_add_lift_rank_le_rank_prod` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `Cardinal.instAdd` `Cardinal.lift` `Module.rank` `Prod.instAddCommMonoid` `Prod.instModule`	—	`rank_ulift` `LE.le.trans_eq` `rank_add_rank_le_rank_prod` `LinearEquiv.rank_eq`
`linearIndepOn_union_iff_quotient` 📖	mathematical	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	`LinearIndepOn` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Set` `Set.instUnion` `HasQuotient.Quotient` `Submodule` `Submodule.hasQuotient` `Submodule.span` `Set.image` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `LinearMap.instFunLike` `Submodule.mkQ`	—	`LinearIndepOn.mono` `Set.subset_union_left` `LinearIndependent.map` `Set.subset_union_right` `Submodule.ker_mkQ` `Disjoint.symm` `linearIndepOn_union_iff` `LinearIndepOn.union_of_quotient`
`rank_add_rank_le_rank_prod` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `Cardinal.instAdd` `Module.rank` `Prod.instAddCommMonoid` `Prod.instModule`	—	`Module.rank_def` `Cardinal.ciSup_add_ciSup` `nonempty_linearIndependent_set` `Cardinal.bddAbove_range` `small_subtype` `small_set` `UnivLE.small` `UnivLE.self` `ciSup_le` `LinearIndependent.cardinal_le_rank` `linearIndependent_inl_union_inr'`
`rank_directSum` 📖	mathematical	`Module.Free`	`Module.rank` `DirectSum` `instAddCommMonoidDirectSum` `DirectSum.instModule` `Cardinal.sum`	—	`Module.Basis.mk_eq_rank''` `Cardinal.mk_sigma`
`rank_fin_fun` 📖	mathematical	—	`Module.rank` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Pi.Function.module` `Semiring.toModule` `Cardinal` `Cardinal.instNatCast`	—	`rank_pi` `Module.Free.self` `Finite.of_fintype` `Module.rank_self` `Cardinal.sum_const` `Cardinal.mk_fintype` `Fintype.card_fin` `Cardinal.lift_natCast` `Cardinal.lift_uzero` `mul_one`
`rank_finsupp` 📖	mathematical	—	`Module.rank` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finsupp.instAddCommMonoid` `Finsupp.module` `Cardinal` `Cardinal.instMul` `Cardinal.lift`	—	`Module.Free.exists_basis` `Module.Basis.mk_eq_rank''` `Cardinal.mk_sigma` `Cardinal.sum_const`
`rank_finsupp'` 📖	mathematical	—	`Module.rank` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finsupp.instAddCommMonoid` `Finsupp.module` `Cardinal` `Cardinal.instMul`	—	`rank_finsupp` `Cardinal.lift_id`
`rank_finsupp_self` 📖	mathematical	—	`Module.rank` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `Cardinal.lift`	—	`rank_finsupp` `Module.Free.self` `Module.rank_self` `Cardinal.lift_one` `mul_one`
`rank_finsupp_self'` 📖	mathematical	—	`Module.rank` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule`	—	`rank_finsupp` `Module.Free.self` `Cardinal.lift_id` `Module.rank_self` `mul_one`
`rank_fun` 📖	mathematical	—	`Module.rank` `Pi.addCommMonoid` `Pi.Function.module` `Cardinal` `Cardinal.instMul` `Cardinal.instNatCast` `Fintype.card`	—	`rank_pi` `Finite.of_fintype` `Cardinal.sum_const'` `Cardinal.mk_fintype`
`rank_fun'` 📖	mathematical	—	`Module.rank` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Pi.Function.module` `Semiring.toModule` `Cardinal` `Cardinal.instNatCast` `Fintype.card`	—	`rank_fun_eq_lift_mul` `Module.Free.self` `Module.rank_self` `Cardinal.lift_one` `mul_one`
`rank_fun_eq_lift_mul` 📖	mathematical	—	`Module.rank` `Pi.addCommMonoid` `Pi.Function.module` `Cardinal` `Cardinal.instMul` `Cardinal.instNatCast` `Fintype.card` `Cardinal.lift`	—	`rank_pi` `Finite.of_fintype` `Cardinal.sum_const` `Cardinal.mk_fintype` `Cardinal.lift_natCast`
`rank_matrix` 📖	mathematical	—	`Module.rank` `Matrix` `Matrix.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Matrix.module` `Semiring.toModule` `Cardinal` `Cardinal.instMul` `Cardinal.lift`	—	`rank_matrix_module` `Module.Free.self` `Module.rank_self` `Cardinal.lift_one` `mul_one` `Cardinal.lift_lift` `Cardinal.lift_id`
`rank_matrix'` 📖	mathematical	—	`Module.rank` `Matrix` `Matrix.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Matrix.module` `Semiring.toModule` `Cardinal.lift` `Cardinal` `Cardinal.instMul`	—	`rank_matrix` `Cardinal.lift_mul` `Cardinal.lift_umax`
`rank_matrix''` 📖	mathematical	—	`Module.rank` `Matrix` `Matrix.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Matrix.module` `Semiring.toModule` `Cardinal` `Cardinal.instMul`	—	`rank_matrix_module'` `Module.Free.self` `Cardinal.lift_id` `Module.rank_self` `mul_one`
`rank_matrix_module` 📖	mathematical	—	`Module.rank` `Matrix` `Matrix.addCommMonoid` `Matrix.module` `Cardinal` `Cardinal.instMul` `Cardinal.lift`	—	`nonempty_fintype` `Module.Free.exists_basis` `Module.Basis.mk_eq_rank''` `Cardinal.mk_prod` `Cardinal.lift_mul` `Cardinal.lift_lift`
`rank_matrix_module'` 📖	mathematical	—	`Module.rank` `Matrix` `Matrix.addCommMonoid` `Matrix.module` `Cardinal` `Cardinal.instMul` `Cardinal.lift`	—	`rank_matrix_module` `Cardinal.lift_mul` `Cardinal.lift_umax`
`rank_pi` 📖	mathematical	`Module.Free`	`Module.rank` `Pi.addCommMonoid` `Pi.module` `Cardinal.sum`	—	`nonempty_fintype` `Module.Basis.mk_eq_rank''` `Cardinal.mk_sigma`
`rank_prod` 📖	mathematical	—	`Module.rank` `Prod.instAddCommMonoid` `Prod.instModule` `Cardinal` `Cardinal.instAdd` `Cardinal.lift`	—	`Module.Free.rank_eq_card_chooseBasisIndex` `Cardinal.lift_id` `Cardinal.mk_sum` `Module.Basis.mk_eq_rank`
`rank_prod'` 📖	mathematical	—	`Module.rank` `Prod.instAddCommMonoid` `Prod.instModule` `Cardinal` `Cardinal.instAdd`	—	`rank_prod` `Cardinal.lift_id`
`rank_quotient_add_rank_le` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `Cardinal.instAdd` `Module.rank` `HasQuotient.Quotient` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.hasQuotient` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module`	—	`Module.rank_def` `Cardinal.ciSup_add_ciSup` `nonempty_linearIndependent_set` `Cardinal.bddAbove_range` `small_subtype` `small_set` `Submodule.Quotient.instSmallQuotient` `UnivLE.small` `UnivLE.self` `ciSup_le` `Cardinal.mk_sum` `Cardinal.lift_id` `add_comm` `LinearIndependent.cardinal_le_rank` `LinearIndependent.sumElim_of_quotient` `Submodule.Quotient.mk_surjective`
`rank_quotient_le` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `Module.rank` `HasQuotient.Quotient` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.hasQuotient` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module`	—	`LinearMap.rank_le_of_surjective` `Quot.mk_surjective`
`rank_span_finset_le` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `Module.rank` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `SetLike.coe` `Finset` `Finset.instSetLike` `Submodule.addCommMonoid` `Submodule.module` `Cardinal.instNatCast` `Finset.card`	—	`Cardinal.mk_fintype` `Fintype.card_coe` `rank_span_le`
`rank_span_le` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `Module.rank` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Submodule.addCommMonoid` `Submodule.module` `Set.Elem`	—	`RingHomSurjective.ids` `Finsupp.span_eq_range_linearCombination` `StrictMono.le_iff_le` `Cardinal.lift_strictMono` `LE.le.trans` `lift_rank_range_le` `rank_finsupp_self` `Cardinal.lift_lift`
`rank_span_of_finset` 📖	mathematical	—	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder` `Module.rank` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `SetLike.coe` `Finset` `Finset.instSetLike` `Submodule.addCommMonoid` `Submodule.module` `Cardinal.aleph0`	—	`LE.le.trans_lt` `rank_span_finset_le` `Cardinal.natCast_lt_aleph0`
`rank_tensorProduct` 📖	mathematical	—	`Module.rank` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `IsScalarTower.to_smulCommClass` `Cardinal` `Cardinal.instMul` `Cardinal.lift` `CommSemiring.toSemiring`	—	`IsScalarTower.to_smulCommClass` `Module.Free.exists_basis` `Module.Basis.mk_eq_rank''` `Cardinal.mk_prod`
`rank_tensorProduct'` 📖	mathematical	—	`Module.rank` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `IsScalarTower.to_smulCommClass` `Cardinal` `Cardinal.instMul` `CommSemiring.toSemiring`	—	`IsScalarTower.to_smulCommClass` `rank_tensorProduct` `Cardinal.lift_id`
`rank_ulift` 📖	mathematical	—	`Module.rank` `ULift.addCommMonoid` `ULift.module'` `Cardinal.lift`	—	`Cardinal.lift_injective` `Cardinal.lift_lift` `LinearEquiv.lift_rank_eq` `RingHomInvPair.ids`
`span_lt_of_subset_of_card_lt_finrank` 📖	mathematical	`Set` `Set.instHasSubset` `SetLike.coe` `Submodule` `Submodule.setLike` `Finset.card` `Set.toFinset` `Module.finrank` `SetLike.instMembership` `Submodule.addCommMonoid` `Submodule.module`	`Submodule` `Preorder.toLT` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Submodule.span`	—	`Submodule.lt_of_le_of_finrank_lt_finrank` `Submodule.span_le` `lt_of_le_of_lt` `finrank_span_le_card`
`span_lt_top_of_card_lt_finrank` 📖	mathematical	`Finset.card` `Set.toFinset` `Module.finrank`	`Submodule` `Preorder.toLT` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Submodule.span` `Top.top` `Submodule.instTop`	—	`Submodule.lt_top_of_finrank_lt_finrank` `lt_of_le_of_lt` `finrank_span_le_card`
`subalgebra_top_finrank_eq_submodule_top_finrank` 📖	mathematical	—	`Module.finrank` `Subalgebra` `SetLike.instMembership` `Subalgebra.instSetLike` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Subalgebra.toSemiring` `Subalgebra.instModuleSubtypeMem` `Submodule` `Algebra.toModule` `Submodule.setLike` `Submodule.instTop` `Submodule.addCommMonoid` `Submodule.module`	—	`Algebra.top_toSubmodule`
`subalgebra_top_rank_eq_submodule_top_rank` 📖	mathematical	—	`Module.rank` `Subalgebra` `SetLike.instMembership` `Subalgebra.instSetLike` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Subalgebra.toSemiring` `Subalgebra.instModuleSubtypeMem` `Submodule` `Algebra.toModule` `Submodule.setLike` `Submodule.instTop` `Submodule.addCommMonoid` `Submodule.module`	—	`Algebra.top_toSubmodule`

---

← Back to Index