Theorems · Theorem · number theory

IsArithFrobAt.mul_inv_mem_inertia

∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {G : Type u_3}
  [inst_3 : Group G] [inst_4 : MulSemiringAction G S] [inst_5 : SMulCommClass G R S] {Q : Ideal S} {σ σ' : G},
  IsArithFrobAt R σ Q → IsArithFrobAt R σ' Q → σ * σ'⁻¹ ∈ Ideal.inertia G Q

Defined in

Mathlib.RingTheory.Frobenius

Cited by

0 results in Mathlib

Foundations

Depth 92 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebraGroupMulSemiringActionSMulCommClass