isRightRegular_up — Mathlib

English

For every a in R, IsRightRegular(ULift.up a) iff IsRightRegular a.

Русский

Для каждого элемента a в R верно: IsRightRegular(ULift.up a) эквивалентно IsRightRegular a.

LaTeX

$$$IsRightRegular(\mathrm{ULift}(a)) \leftrightarrow IsRightRegular(a)$$$

Lean4

@[to_additive (attr := simp)]
theorem isRightRegular_up {a : R} : IsRightRegular (ULift.up.{u} a) ↔ IsRightRegular a :=
  Equiv.ulift.symm.comp_injective _ |>.trans <| Equiv.ulift.symm.injective_comp _ |>.symm

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