isUnit_aeval_of_isUnit_aeval_of_isNilpotent_sub

English

If hb is IsUnit (aeval b P) and hab is IsNilpotent (a − b), then IsUnit (aeval a P).

Русский

Если hb — единица для aeval b P, а hab — нильпотентность (a − b), то IsUnit (aeval a P).

LaTeX

$$$\operatorname{IsUnit}(\operatorname{aeval}(b, P)) \land \operatorname{IsNilpotent}(a - b) \Rightarrow \operatorname{IsUnit}(\operatorname{aeval}(a, P))$$$

Lean4

theorem isUnit_aeval_of_isUnit_aeval_of_isNilpotent_sub (hb : IsUnit (aeval b P)) (hab : IsNilpotent (a - b)) :
    IsUnit (aeval a P) := by
  rw [← add_sub_cancel (aeval b P) (aeval a P)]
  refine IsNilpotent.isUnit_add_left_of_commute ?_ hb (Commute.all _ _)
  exact isNilpotent_aeval_sub_of_isNilpotent_sub P hab

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