self_mul_dual — Mathlib

English

Equivalently, I · dual(I) = dual(1) when I is nonzero; note commutativity yields the same product as in the previous item.

Русский

Аналогично, если I ≠ 0, тогда I · dual(I) = dual(1); из-за коммутативности результат совпадает с предыдущим пунктом.

LaTeX

$$I \cdot \mathrm{dual}_{A,K}(I) = \mathrm{dual}_{A,K}(1)$$

Lean4

theorem self_mul_dual (hI : I ≠ 0) : I * dual A K I = dual A K 1 := by rw [mul_comm, dual_mul_self A K hI]

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