coe_dual_one

Mathlib.RingTheory.DedekindDomain.Different

URI: https://scilib.ai/kg/mathlib#FractionalIdeal.coe_dual_one

English

Thecoe dual of 1 equals 1ᵛ in the submodule sense: the coe_dual of one is the dual of one.

Русский

Коэ дуал единицы совпадает с дуалью единицы на подмодуле.

LaTeX

$$coe_dual_one : (dual A K (1 : FractionalIdeal B⁰ L) : Submodule B L) = 1ᵛ.$$

Lean4

@[simp]
theorem coe_dual_one : (dual A K (1 : FractionalIdeal B⁰ L) : Submodule B L) = 1ᵛ :=
  by
  rw [← coe_one, coe_dual]
  exact one_ne_zero

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

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

Разделы

Аффилиация

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