Action

📁 Source: Mathlib/LinearAlgebra/Projectivization/Action.lean

Statistics

Metric	Count
Definitions instMulAction	1
Theorems generalLinearGroup_smul_def, smul_def, smul_mk	3
Total	4

Projectivization

Definitions

Name	Category	Theorems
instMulAction 📖	CompOp	3 math math: smul_def, generalLinearGroup_smul_def, smul_mk

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
generalLinearGroup_smul_def 📖	mathematical	—	LinearMap.GeneralLinearGroup DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid Projectivization SemigroupAction.toSMul Monoid.toSemigroup Units.instMonoid LinearMap RingHom.id Semiring.toNonAssocSemiring Module.End.instMonoid MulAction.toSemigroupAction instMulAction Units.instGroup Units.instDistribMulAction SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Module.toDistribMulAction Module.End.instSemiring Module.End.applyModule Units.smulCommClass_left SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.End.apply_smulCommClass' AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid map LinearEquiv.toLinearMap RingHomInvPair.ids LinearMap.GeneralLinearGroup.toLinearEquiv LinearEquiv.injective	—	Units.smulCommClass_left Module.End.apply_smulCommClass' IsScalarTower.left
smul_def 📖	mathematical	—	Projectivization SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction instMulAction map RingHom.id Semiring.toNonAssocSemiring DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring DFunLike.coe MonoidHom Module.End AddCommGroup.toAddCommMonoid MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike DistribMulAction.toModuleEnd	—	—
smul_mk 📖	mathematical	—	Projectivization SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction instMulAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul smul_ne_zero_iff_ne	—	—

---

← Back to Index