annihilator_smul — Mathlib

English

For any N, we have Ann_R(N) · N = ⊥ (the product is the zero submodule).

Русский

Для любого N имеем Ann_R(N) · N = ⊥ (полезное свойство: произведение на аннигилятор даёт нулевой подмодуль).

LaTeX

$$$ \\operatorname{Ann}_R(N) \\cdot N = \\bot. $$$

Lean4

@[simp]
theorem annihilator_smul (N : Submodule R M) : annihilator N • N = ⊥ :=
  eq_bot_iff.2 (smul_le.2 fun _ => mem_annihilator.1)

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