eq

Mathlib.Algebra.Lie.Ideal

URI: https://scilib.ai/kg/mathlib#LieHom.IsIdealMorphism.eq

English

If f is an ideal morphism, then the ideal-range equals the actual range of f.

Русский

Если f является идеальным морфизмом, то диапазон идеала совпадает с обычным диапазоном f.

LaTeX

$$$ f.IsIdealMorphism \\Rightarrow f.idealRange = f.range $$$

Lean4

theorem eq (hf : f.IsIdealMorphism) : f.idealRange = f.range :=
  hf

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru