isEquiv_trivial_iff_eq_trivial — Mathlib

English

An absolute value is equivalent to the trivial one iff it is the trivial absolute value itself.

Русский

Абсолютное значение эквивалентно тривиальному тогда и только тогда, когда оно само тривиально.

LaTeX

$$$ (v \ IsEquiv \; v_{\text{trivial}}) \iff (v = v_{\text{trivial}}) $$$

Lean4

/-- An absolute value is equivalent to the trivial iff it is trivial itself. -/
@[simp]
theorem isEquiv_trivial_iff_eq_trivial [DecidablePred fun x : R ↦ x = 0] [NoZeroDivisors R] [IsStrictOrderedRing S]
    {f : AbsoluteValue R S} : f.IsEquiv .trivial ↔ f = .trivial :=
  ⟨fun h ↦ by aesop (add simp [h.eq_one_iff, AbsoluteValue.trivial]), fun h ↦ h ▸ .rfl⟩

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