English
The identity between ZMod m and ZMod n when m = n, as a ring isomorphism.
Русский
Идентичность между ZMod m и ZMod n при m = n в виде кольцевого изоморфизма.
LaTeX
$$$ ZMod m \cong+* ZMod n $ при m = n$$
Lean4
/-- The identity between `ZMod m` and `ZMod n` when `m = n`, as a ring isomorphism. -/
def ringEquivCongr {m n : ℕ} (h : m = n) : ZMod m ≃+* ZMod n :=
by
rcases m with - | m <;> rcases n with - | n
· exact RingEquiv.refl _
· exfalso
exact n.succ_ne_zero h.symm
· exfalso
exact m.succ_ne_zero h
·
exact
{
finCongr
h with
map_mul' := fun a b => by
dsimp [ZMod]
ext
rw [Fin.coe_cast, Fin.coe_mul, Fin.coe_mul, Fin.coe_cast, Fin.coe_cast, ← h]
map_add' := fun a b => by
dsimp [ZMod]
ext
rw [Fin.coe_cast, Fin.val_add, Fin.val_add, Fin.coe_cast, Fin.coe_cast, ← h] }
