coe_one — Mathlib

English

The identity element of the ambient ring M, when viewed as an element of the L-projection subtype, coincides with the identity in M; i.e., the underlying element of 1 is the ring identity.

Русский

Единичный элемент внешнего кольца M, рассматривая как элемент подмножества L-проекций, совпадает с единицей кольца; то есть подлежащий элемент 1 в подмножестве соответствует единице в M.

LaTeX

$$$\uparrow(1) = 1\quad\text{in } M.$$$$

Lean4

@[simp]
theorem coe_one : ↑(1 : { P : M // IsLprojection X P }) = (1 : M) :=
  rfl

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