ringEquivCongr_symm

Mathlib.Data.ZMod.Basic

URI: https://scilib.ai/kg/mathlib#ZMod.ringEquivCongr_symm

English

If a = b, then (ringEquivCongr a=b).symm = ringEquivCongr b=a.

Русский

Если a = b, то (ringEquivCongr a=b).symm = ringEquivCongr b=a.

LaTeX

$$$ (ringEquivCongr\, hab).symm = ringEquivCongr\, hab.symm $$$

Lean4

theorem ringEquivCongr_symm {a b : ℕ} (hab : a = b) : (ringEquivCongr hab).symm = ringEquivCongr hab.symm :=
  by
  subst hab
  cases a <;> rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru