zero_quot

Mathlib.Algebra.RingQuot

URI: https://scilib.ai/kg/mathlib#RingQuot.zero_quot

English

The zero element of the quotient is the class of zero: 0_{Quot} = [0].

Русский

Ноль в кольце-остатке равен классу нуля: 0_{Quot} = [0].

LaTeX

$$$0_{\mathrm{Quot}(R,r)} = \overline{0_R}$$$

Lean4

theorem zero_quot : (⟨Quot.mk _ 0⟩ : RingQuot r) = 0 :=
  show _ = zero r by rw [zero_def]

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

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

Разделы

Аффилиация

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