semifield — Mathlib

English

Nonzero fractional ideals are invertible; I · I^{-1} = 1.

Русский

Не нулевые дробные идеалы обратимы; I · I^{-1} = 1.

LaTeX

$$$$I \\neq 0 \\Rightarrow I \\cdot I^{-1} = 1.$$$$

Lean4

noncomputable instance semifield : Semifield (FractionalIdeal A⁰ K)
    where
  __ := coeIdeal_injective.nontrivial
  inv_zero := inv_zero' _
  div_eq_mul_inv := FractionalIdeal.div_eq_mul_inv
  mul_inv_cancel _ := FractionalIdeal.mul_inv_cancel
  nnqsmul := _
  nnqsmul_def := fun _ _ => rfl

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