Aut

📁 Source: Mathlib/Algebra/Ring/Aut.lean

Statistics

Metric	Count
Definitions RingAut, instGroup, instInhabited, toAddAut, toMulAut, toPerm	6
Theorems coe_one, coe_pow, inv_apply, mul_apply, one_apply, one_eq_refl	6
Total	12

RingAut

Definitions

Name	Category	Theorems
instGroup 📖	CompOp	24 math math: one_eq_refl, cyclotomicCharacter.toZModPow, smul_def, modularCyclotomicCharacter.spec, IsPrimitiveRoot.autToPow_eq_modularCyclotomicCharacter, iterateFrobeniusEquiv_eq_pow, one_apply, MulSemiringAction.toRingAut_apply, WittVector.dvd_sub_sum_teichmuller_iterateFrobeniusEquiv_coeff, iterateFrobeniusEquiv_symm, modularCyclotomicCharacter.unique, Ideal.pointwise_smul_eq_comap, inv_apply, coe_one, cyclotomicCharacter.toZModPow_toFun, IsLocalRing.ResidueField.mapAut_apply, modularCyclotomicCharacter.comp, cyclotomicCharacter.spec, apply_faithfulSMul, modularCyclotomicCharacter'.spec', mul_apply, modularCyclotomicCharacter'.unique', cyclotomicCharacter.continuous, coe_pow
instInhabited 📖	CompOp	—
toAddAut 📖	CompOp	—
toMulAut 📖	CompOp	—
toPerm 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_one 📖	mathematical	—	DFunLike.coe RingEquiv EquivLike.toFunLike RingEquiv.instEquivLike InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid instGroup	—	—
coe_pow 📖	mathematical	—	DFunLike.coe RingEquiv EquivLike.toFunLike RingEquiv.instEquivLike Monoid.toNatPow DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup Nat.iterate	—	pow_zero pow_succ
inv_apply 📖	mathematical	—	DFunLike.coe RingEquiv EquivLike.toFunLike RingEquiv.instEquivLike InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid instGroup RingEquiv.symm	—	—
mul_apply 📖	mathematical	—	DFunLike.coe RingEquiv EquivLike.toFunLike RingEquiv.instEquivLike MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup	—	—
one_apply 📖	mathematical	—	DFunLike.coe RingEquiv EquivLike.toFunLike RingEquiv.instEquivLike InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid instGroup	—	—
one_eq_refl 📖	mathematical	—	RingEquiv InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid instGroup RingEquiv.refl	—	—

(root)

Definitions

Name	Category	Theorems
RingAut 📖	CompOp	5 math math: RingAut.smul_def, MulSemiringAction.toRingAut_apply, Ideal.pointwise_smul_eq_comap, IsLocalRing.ResidueField.mapAut_apply, RingAut.apply_faithfulSMul

---

← Back to Index