instHPowNat

Mathlib.RingTheory.Ideal.Operations

URI: https://scilib.ai/kg/mathlib#Ideal.IsTwoSided.instHPowNat

← MathLib Explorer

English

If I ≤ J then I ⋅ K ≤ J ⋅ K.

Русский

Если I ≤ J, то I⋅K ≤ J⋅K.

LaTeX

$$$I \cdot K \le J \cdot K$$$

Lean4

instance (priority := low) : (I ^ n).IsTwoSided :=
  n.rec (by rw [Submodule.pow_zero, one_eq_top]; infer_instance) (fun _ _ ↦ by rw [Submodule.pow_succ]; infer_instance)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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