Documentation Verification Report

End

📁 Source: Mathlib/Algebra/Ring/Action/End.lean

Statistics

Metric	Count
Definitions `toRingAut`, `applyMulSemiringAction`	2
Theorems `toRingAut_apply`, `apply_faithfulSMul`, `smul_def`	3
Total	5

MulSemiringAction

Definitions

Name	Category	Theorems
`toRingAut` 📖	CompOp	3 math math: `toRingAut_apply`, `Ideal.pointwise_smul_eq_comap`, `cyclotomicCharacter.continuous`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toRingAut_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `RingAut` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toAdd` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `RingAut.instGroup` `MonoidHom.instFunLike` `toRingAut` `toRingEquiv`	—	—

RingAut

Definitions

Name	Category	Theorems
`applyMulSemiringAction` 📖	CompOp	2 math math: `smul_def`, `apply_faithfulSMul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_faithfulSMul` 📖	mathematical	—	`FaithfulSMul` `RingAut` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toAdd` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup` `MulSemiringAction.toDistribMulAction` `applyMulSemiringAction`	—	`RingEquiv.ext`
`smul_def` 📖	mathematical	—	`RingAut` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toAdd` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup` `MulSemiringAction.toDistribMulAction` `applyMulSemiringAction` `DFunLike.coe` `EquivLike.toFunLike` `RingEquiv.instEquivLike`	—	—

---

← Back to Index