mulShift_unit_eq_one_iff — Mathlib

English

Let u be a unit in R. Then mulShift ψ u = 1 if and only if ψ = 1 (under the unit hypothesis).

Русский

Пусть u является единицей в R. Тогда mulShift ψ u = 1 тогда же ψ = 1 (при условии, что u единица).

LaTeX

$$$IsUnit(u) \Rightarrow (mulShift(ψ, u) = 1 \Leftrightarrow ψ = 1)$$$

Lean4

theorem mulShift_unit_eq_one_iff (ψ : AddChar R M) {u : R} (hu : IsUnit u) : ψ.mulShift u = 1 ↔ ψ = 1 :=
  by
  refine ⟨fun h ↦ ?_, ?_⟩
  · ext1 y
    rw [show y = u * (hu.unit⁻¹ * y) by rw [← mul_assoc, IsUnit.mul_val_inv, one_mul]]
    simpa only [mulShift_apply] using DFunLike.ext_iff.mp h (hu.unit⁻¹ * y)
  · solve_by_elim

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