sec_zero_fst — Mathlib

English

For a localization map f, the value of f on the first component of the representation of 0 is 0; equivalently, f((sec 0).fst) = 0.

Русский

Для локализационной карты f значение на первой компоненте разложения нуля равно 0; то есть f((sec 0).fst) = 0.

LaTeX

$$$f((f.sec\,0).\text{fst}) = 0$$$

Lean4

@[simp]
theorem sec_zero_fst {f : LocalizationMap S N} : f (f.sec 0).fst = 0 := by rw [LocalizationMap.sec_spec', mul_zero]

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