inverse_star — Mathlib

English

Star-inverse commutes with inverse: star of inv r equals inv of star r, under invertibility assumptions.

Русский

Звезда-противоположность инверсуется с обратной стороны: звезда inv(r) равна inv(star(r)).

LaTeX

$$$\star(\,r^{ -1 }\,) = (\star r)^{ -1 }$ при условиях инвертируемости.$$

Lean4

theorem inverse_star [Semiring R] [StarRing R] (a : R) : Ring.inverse (star a) = star (Ring.inverse a) :=
  by
  by_cases ha : IsUnit a
  · obtain ⟨u, rfl⟩ := ha
    rw [Ring.inverse_unit, ← Units.coe_star, Ring.inverse_unit, ← Units.coe_star_inv]
  rw [Ring.inverse_non_unit _ ha, Ring.inverse_non_unit _ (mt isUnit_star.mp ha), star_zero]

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