isUnit_ι_of_isUnit — Mathlib

English

If Q(m) is a unit in the base ring, then the embedding ι_Q(m) is a unit in the corresponding endomorphism algebra.

Русский

Если Q(m) является единицей в базовой кольцевой структуре, то вложение ι_Q(m) является единицей в соответствующем алгебраическом конструкте.

LaTeX

$$isUnit_ι_of_isUnit(Q,m)$$

Lean4

theorem isUnit_ι_of_isUnit {m : M} (h : IsUnit (Q m)) : IsUnit (ι Q m) :=
  by
  cases h.nonempty_invertible
  letI := invertibleιOfInvertible Q m
  exact isUnit_of_invertible (ι Q m)

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