idealFactorsEquivOfQuotEquiv_symm

Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

URI: https://scilib.ai/kg/mathlib#idealFactorsEquivOfQuotEquiv_symm

English

The symmetry of the quotient factor bijection: the symm of idealFactorsEquivOfQuotEquiv f equals idealFactorsEquivOfQuotEquiv f.symm.

Русский

Симметрия биекции факторов деления: симм idealFactorsEquivOfQuotEquiv f равна f.symm.

LaTeX

$$idealFactorsEquivOfQuotEquiv_symm$$

Lean4

theorem idealFactorsEquivOfQuotEquiv_symm :
    (idealFactorsEquivOfQuotEquiv f).symm = idealFactorsEquivOfQuotEquiv f.symm :=
  rfl

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

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

Разделы

Аффилиация

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