Matrix

📁 Source: Mathlib/LinearAlgebra/FreeModule/Finite/Matrix.lean

Statistics

Metric	Count
Definitions	0
Theorems algHom, addMonoidHom, linearMap, addMonoidHom, linearMap, finrank_linearMap, finrank_linearMap_self, rank_linearMap, rank_linearMap_self, card_algHom_le_finrank, cardinalMk_algHom_le_rank	11
Total	11

Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algHom 📖	mathematical	—	Finite AlgHom CommRing.toCommSemiring Ring.toSemiring CommSemiring.toSemiring	—	LinearIndependent.finite Algebra.to_smulCommClass commRing_strongRankCondition IsDomain.toNontrivial Module.Finite.linearMap Module.Finite.self linearIndependent_algHom_toLinearMap

Module

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finrank_linearMap 📖	mathematical	—	finrank LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.addCommMonoid LinearMap.module	—	rank_linearMap Cardinal.toNat_mul Cardinal.toNat_lift
finrank_linearMap_self 📖	mathematical	—	finrank LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing LinearMap.addCommMonoid LinearMap.module Semiring.toModule	—	finrank_linearMap Free.self finrank_self mul_one
rank_linearMap 📖	mathematical	—	rank LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.addCommMonoid LinearMap.module Cardinal Cardinal.instMul Cardinal.lift	—	LinearEquiv.rank_eq rank_fun_eq_lift_mul finrank_eq_card_chooseBasisIndex finrank_eq_rank Cardinal.lift_natCast
rank_linearMap_self 📖	mathematical	—	rank LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing LinearMap.addCommMonoid LinearMap.module Semiring.toModule Cardinal.lift	—	rank_linearMap Free.self rank_self Cardinal.lift_one mul_one

Module.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addMonoidHom 📖	mathematical	—	Module.Finite AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Int.instSemiring AddMonoidHom.instAddCommMonoid AddCommGroup.toAddCommMonoid AddCommGroup.toIntModule AddMonoidHom.instAddCommGroup	—	equiv AddGroup.int_smulCommClass linearMap RingHomInvPair.ids
linearMap 📖	mathematical	—	Module.Finite LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.addCommMonoid LinearMap.module	—	equiv pi Finite.of_fintype RingHomInvPair.ids

Module.Free

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addMonoidHom 📖	mathematical	—	Module.Free AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Int.instSemiring AddMonoidHom.instAddCommMonoid AddCommGroup.toAddCommMonoid AddCommGroup.toIntModule AddMonoidHom.instAddCommGroup	—	of_equiv AddGroup.int_smulCommClass linearMap RingHomInvPair.ids
linearMap 📖	mathematical	—	Module.Free LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.addCommMonoid LinearMap.module	—	of_equiv function Finite.of_fintype RingHomInvPair.ids

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_algHom_le_finrank 📖	mathematical	—	Nat.card AlgHom CommRing.toCommSemiring Ring.toSemiring CommSemiring.toSemiring Module.finrank NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule	—	Cardinal.toNat_lift Module.finrank.eq_1 Cardinal.toNat_le_toNat cardinalMk_algHom_le_rank Cardinal.lift_lt_aleph0 Module.nontrivial IsDomain.toNontrivial Module.rank_lt_aleph0 commRing_strongRankCondition
cardinalMk_algHom_le_rank 📖	mathematical	—	Cardinal Cardinal.instLE AlgHom CommRing.toCommSemiring Ring.toSemiring CommSemiring.toSemiring Cardinal.lift Module.rank NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule	—	Algebra.to_smulCommClass Cardinal.lift_id Module.nontrivial IsDomain.toNontrivial Module.rank_linearMap_self commRing_strongRankCondition LinearIndependent.cardinal_lift_le_rank linearIndependent_algHom_toLinearMap

---

← Back to Index