smul_iff

Mathlib.RingTheory.Ideal.Pointwise

URI: https://scilib.ai/kg/mathlib#Ideal.IsPrime.smul_iff

English

For any I, (g • I) is prime if and only if I is prime.

Русский

Для любого I выполяется: (g • I) прост тогда и только тогда, когда I прост.

LaTeX

$$$\forall I \in \text{Ideal}(R)\, \forall g \in M:\ (g \cdot I).IsPrime \iff I.IsPrime$$$

Lean4

@[simp]
theorem smul_iff {I : Ideal R} (g : M) : (g • I).IsPrime ↔ I.IsPrime :=
  ⟨fun H ↦ inv_smul_smul g I ▸ H.smul g⁻¹, fun H ↦ H.smul g⟩

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

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

Разделы

Аффилиация

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