instIsTwoSidedColon — Mathlib

English

There is an instance showing N.colon P is a two-sided ideal of R.

Русский

Существует инстанс, доказывающий, что N.colon P является двусторонним идеалом по отношению к R.

LaTeX

$$IsTwoSided$ (N.colon P)$$$

Lean4

instance (priority := low) : (N.colon P).IsTwoSided where
  mul_mem_of_left {r} s hr p
    hp := by
    obtain ⟨p, hp, rfl⟩ := hp
    exact hr ⟨_, P.smul_mem _ hp, (mul_smul ..).symm⟩

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