Center

📁 Source: Mathlib/LinearAlgebra/Center.lean

Statistics

Metric	Count
Definitions	0
Theorems commute_transvections_iff_of_basis, exists_eq_smul_id_of_forall_notLinearIndependent, exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent, exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent_of_basis	4
Total	4

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
commute_transvections_iff_of_basis 📖	mathematical	Commute LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Module.End.instMul transvection Module.Basis.coord SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction DFunLike.coe Module.Basis Module.Basis.instFunLike	Subring SetLike.instMembership Subring.instSetLike Subring.center instSMul CommSemiring.toSemiring CommRing.toCommSemiring Subring.instCommRingSubtypeMemCenter AddCommMonoid.toAddMonoid Subring.instDistribMulActionSubtypeMem Subring.instSMulCommClassSubtypeMemCenter DistribMulAction.toMulAction Module.End.instOne	—	Subring.instSMulCommClassSubtypeMemCenter subsingleton_or_nontrivial mul_one one_mul ext one_smul RingHomInvPair.ids Module.Basis.repr_self Finsupp.single_eq_same map_add SemilinearMapClass.toAddHomClass semilinearMapClass map_smul SemilinearMapClass.toMulActionSemiHomClass AddLeftCancelSemigroup.toIsLeftCancelAdd ext_iff exists_ne Nontrivial.to_nonempty Module.Basis.linearCombination_repr Finsupp.linearCombination_apply map_finsuppSum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass Finsupp.smul_sum Finsupp.sum_congr
exists_eq_smul_id_of_forall_notLinearIndependent 📖	mathematical	LinearIndependent Matrix.vecCons DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instFunLike Matrix.vecEmpty	instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing Module.End.instOne	—	smulCommClass_self finrank_eq_one_iff commRing_strongRankCondition IsDomain.toNontrivial Module.Basis.ext RingHomInvPair.ids Module.Basis.linearCombination_repr Finsupp.linearCombination_unique Subring.instSMulCommClassSubtypeMemCenter exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent
exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent 📖	mathematical	LinearIndependent Matrix.vecCons DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instFunLike Matrix.vecEmpty	Subring SetLike.instMembership Subring.instSetLike Subring.center instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Subring.instCommRingSubtypeMemCenter AddCommMonoid.toAddMonoid Subring.instDistribMulActionSubtypeMem Module.toDistribMulAction Subring.instSMulCommClassSubtypeMemCenter DistribMulAction.toMulAction Module.End.instOne	—	Subring.instSMulCommClassSubtypeMemCenter subsingleton_or_nontrivial AddSubmonoidWithOneClass.toOneMemClass SubsemiringClass.addSubmonoidWithOneClass SubringClass.toSubsemiringClass Subring.instSubringClass ext Module.Free.instNonemptyChooseBasisIndexOfNontrivial Finite.of_subsingleton Module.finrank_eq_card_basis Nat.card_unique exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent_of_basis
exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent_of_basis 📖	mathematical	LinearIndependent Matrix.vecCons DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instFunLike Matrix.vecEmpty	Subring SetLike.instMembership Subring.instSetLike Subring.center instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Subring.instCommRingSubtypeMemCenter AddCommMonoid.toAddMonoid Subring.instDistribMulActionSubtypeMem Module.toDistribMulAction Subring.instSMulCommClassSubtypeMemCenter DistribMulAction.toMulAction Module.End.instOne	—	RingHomInvPair.ids Module.Basis.ext_elem_iff map_smul SemilinearMapClass.toMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass Module.Basis.repr_self Finsupp.smul_single mul_one Finsupp.single_apply map_add SemilinearMapClass.toAddHomClass Finsupp.single_eq_of_ne' zero_add map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass IsDomain.to_noZeroDivisors Mathlib.Tactic.Contrapose.contrapose₄ Mathlib.Tactic.Contrapose.contrapose₂ LinearIndependent.eq_of_smul_apply_eq_smul_apply Module.Basis.linearIndependent zero_smul add_zero Module.Basis.repr_symm_apply add_right_cancel_iff AddRightCancelSemigroup.toIsRightCancelAdd Finsupp.sum_update_add add_smul Finsupp.sum_single_index one_smul Finsupp.single_eq_same Finsupp.single_eq_of_ne semilinearMapClass Module.Basis.coord_apply add_eq_zero_iff_eq_neg mul_assoc add_assoc mul_add Distrib.leftDistribClass MulZeroClass.mul_zero neg_zero add_right_comm sub_eq_zero mul_eq_zero mul_sub neg_add_eq_sub neg_mul Mathlib.Tactic.Contrapose.contrapose₃ MulZeroClass.zero_mul one_mul Nontrivial.to_nonempty exists_ne commute_iff_eq Subring.instSMulCommClassSubtypeMemCenter Module.Basis.ext

---

← Back to Index