Commit 2025-02-14 19:33 e829a106

View on Github →

feat(RingTheory): frobenius elements (#21770)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/CharP/Algebra.lean

added theorem CharP.dvd_of_ringHom

added theorem CharP.of_ringHom_of_ne_zero

Modified Mathlib/Algebra/Group/Subgroup/Basic.lean

added def AddSubgroup.inertia

added theorem AddSubgroup.mem_inertia

Created Mathlib/RingTheory/Frobenius.lean

added theorem AlgHom.IsArithFrobAt.apply_of_pow_eq_one

added theorem AlgHom.IsArithFrobAt.card_pos

added theorem AlgHom.IsArithFrobAt.comap_eq

added theorem AlgHom.IsArithFrobAt.eq_of_isUnramifiedAt

added theorem AlgHom.IsArithFrobAt.finite_quotient

added theorem AlgHom.IsArithFrobAt.isArithFrobAt_localize

added theorem AlgHom.IsArithFrobAt.le_comap

added def AlgHom.IsArithFrobAt.localize

added theorem AlgHom.IsArithFrobAt.localize_algebraMap

added theorem AlgHom.IsArithFrobAt.mk_apply

added def AlgHom.IsArithFrobAt.restrict

added theorem AlgHom.IsArithFrobAt.restrict_apply

added theorem AlgHom.IsArithFrobAt.restrict_injective

added theorem AlgHom.IsArithFrobAt.restrict_mk

added def AlgHom.IsArithFrobAt

added theorem IsArithFrobAt.conj

added theorem IsArithFrobAt.exists_of_isInvariant

added theorem IsArithFrobAt.exists_primesOver_isConj

added theorem IsArithFrobAt.mul_inv_mem_inertia

added def arithFrobAt

added theorem isConj_arithFrobAt

Modified Mathlib/RingTheory/Invariant.lean

Modified Mathlib/RingTheory/Localization/Defs.lean

added theorem IsLocalization.mk'_neg

added theorem IsLocalization.mk'_sub

Modified Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean

Modified Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean

added theorem IsPrimitiveRoot.existsUnique

added theorem IsPrimitiveRoot.exists_pos

modified theorem IsPrimitiveRoot.nthRoots_one_eq_biUnion_primitiveRoots'

modified theorem IsPrimitiveRoot.nthRoots_one_eq_biUnion_primitiveRoots

added theorem IsPrimitiveRoot.«exists»

Modified Mathlib/RingTheory/Unramified/Basic.lean

added theorem Algebra.FormallyUnramified.ext_of_iInf

Modified Mathlib/RingTheory/Unramified/Locus.lean