mulRingNormEquivAbsoluteValue — Mathlib

English

There is an equivalence between MulRingNorm R and AbsoluteValue R ℝ when R is a nontrivial ring.

Русский

Существует эквивалентность между MulRingNorm R и AbsoluteValue R ℝ, если R является ненулевым кольцом.

LaTeX

$$$ MulRingNorm R \cong AbsoluteValue R \mathbb{R} $$$

Lean4

/-- The equivalence of `MulRingNorm R` and `AbsoluteValue R ℝ` when `R` is a nontrivial ring. -/
def mulRingNormEquivAbsoluteValue : MulRingNorm R ≃ AbsoluteValue R ℝ
    where
  toFun
    N :=
    { toFun := N.toFun
      map_mul' := N.map_mul'
      nonneg' := apply_nonneg N
      eq_zero' x := ⟨N.eq_zero_of_map_eq_zero' x, fun h ↦ h ▸ N.map_zero'⟩
      add_le' := N.add_le' }
  invFun
    v :=
    { toFun := v.toFun
      map_zero' := (v.eq_zero' 0).mpr rfl
      add_le' := v.add_le'
      neg' := v.map_neg
      map_one' := v.map_one
      map_mul' := v.map_mul'
      eq_zero_of_map_eq_zero' x := (v.eq_zero' x).mp }
  left_inv N := by constructor
  right_inv v := by ext1 x; simp

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