dual_div_dual — Mathlib

English

For fractional ideals I and J, the quotient of their duals is the inverse relation: (dual J)/(dual I) = I/J.

Русский

Для дробных идеалов I и J отношение дуалов даёт взаимную связь: (dual J)/(dual I) = I/J.

LaTeX

$$\frac{\mathrm{dual}_{A,K}(J)}{\mathrm{dual}_{A,K}(I)} = \frac{I}{J}$$

Lean4

theorem dual_div_dual : dual A K J / dual A K I = I / J :=
  by
  rw [dual_eq_mul_inv A K J, dual_eq_mul_inv A K I, mul_div_mul_comm, div_self, one_mul]
  · exact inv_div_inv J I
  · simp only [ne_eq, dual_eq_zero_iff, one_ne_zero, not_false_eq_true]

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