instCanLiftTwoSidedIdealCoeOrderHomAsIdealIsTwoSided

Mathlib.RingTheory.TwoSidedIdeal.Operations

URI: https://scilib.ai/kg/mathlib#Ideal.instCanLiftTwoSidedIdealCoeOrderHomAsIdealIsTwoSided

English

Another instance asserting the CanLift property for the same two map scenario.

Русский

Еще один экземпляр, утверждающий свойство CanLift для данного сценария отображения.

LaTeX

$$same as CanLift above$$

Lean4

instance : CanLift (Ideal R) (TwoSidedIdeal R) TwoSidedIdeal.asIdeal (·.IsTwoSided) where
  prf I _ := ⟨I.toTwoSided, asIdeal_toTwoSided ..⟩

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

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

Разделы

Аффилиация

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