English
In a ring of characteristic p, if n ∈ ℕ is coprime to p, then (n : R) is invertible with inverse n.gcdA p.
Русский
В кольце характеристики p число n, взаимно простое с p, обратимо в R, и его обратное равно n.gcdA p (посчитанное как элемент R).
LaTeX
$$$n.Coprime p \Rightarrow (n : R)^{-1} = (n.gcdA p)^{\mathrm{cast}}$$$
Lean4
/-- In a ring of characteristic `p`, `(n : R)` is invertible when `n` is coprime with `p`, with
inverse `n.gcdA p`. -/
def invertibleOfCoprime {n : ℕ} (h : n.Coprime p) : Invertible (n : R)
where
invOf := n.gcdA p
invOf_mul_self := by rw [CharP.natCast_gcdA_mul_intCast_eq_gcd, h, Nat.cast_one]
mul_invOf_self := by rw [CharP.intCast_mul_natCast_gcdA_eq_gcd, h, Nat.cast_one]
