cast_isEquivalence — Mathlib

English

If the radicals of J and K are equal, the cast functor between SelfLERadical J and SelfLERadical K is an equivalence.

Русский

Если радикалы J и K равны, функтор приведения между SelfLERadical J и SelfLERadical K является эквивалентностью.

LaTeX

$$SelfLERadical.cast hJK).IsEquivalence$$

Lean4

instance cast_isEquivalence (hJK : J.radical = K.radical) : (SelfLERadical.cast hJK).IsEquivalence :=
  (castEquivalence hJK).isEquivalence_functor

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