coe_unit_eq_one

Mathlib.Algebra.GroupWithZero.Associated

URI: https://scilib.ai/kg/mathlib#Associates.coe_unit_eq_one

English

Every unit of the quotient maps to the unit element 1.

Русский

Любая единица в квотиенте отображается в элемент единицы 1.

LaTeX

$$$ \forall u : (\operatorname{Associates}(M))^{\times}, (u : \operatorname{Associates}(M)) = 1 $$$

Lean4

@[simp]
theorem coe_unit_eq_one (u : (Associates M)ˣ) : (u : Associates M) = 1 := by simp [eq_iff_true_of_subsingleton]

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

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

Разделы

Аффилиация

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