ringEquivOfPrime_eq_ringEquiv — Mathlib

English

The two isomorphisms defined by ringEquivOfPrime and ringEquiv coincide: ringEquivOfPrime R hp hR = ringEquiv R hR.

Русский

Два изоморфизма, заданные ringEquivOfPrime и ringEquiv, совпадают: ringEquivOfPrime R hp hR = ringEquiv R hR.

LaTeX

$$$ ringEquivOfPrime\, R\, hp\, hR = ringEquiv R hR $$$

Lean4

@[simp]
theorem ringEquivOfPrime_eq_ringEquiv [Fintype R] {p : ℕ} [CharP R p] (hp : p.Prime) (hR : Fintype.card R = p) :
    ringEquivOfPrime R hp hR = ringEquiv R hR :=
  rfl

Похожие утверждения