cotangentIdeal_square — Mathlib

English

The square of the cotangent ideal is the bottom submodule: I.cotangentIdeal^2 = ⊥.

Русский

Квадрат котонтантного идеала равен нулевому подмодулю: I.cotangentIdeal^2 = ⊥.

LaTeX

$$$I.cotangentIdeal^2 = \\bot$$$

Lean4

theorem cotangentIdeal_square (I : Ideal R) : I.cotangentIdeal ^ 2 = ⊥ :=
  by
  rw [eq_bot_iff, pow_two I.cotangentIdeal, ← smul_eq_mul]
  intro x hx
  refine Submodule.smul_induction_on hx ?_ ?_
  · rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩; apply (Submodule.Quotient.eq _).mpr _
    rw [sub_zero, pow_two]; exact Ideal.mul_mem_mul hx hy
  · intro x y hx hy; exact add_mem hx hy

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