le_annihilator_iff — Mathlib

English

The annihilator of a submodule N is the set of scalars killing all of N; equivalently, r ∈ Ann_R(N) iff r·n = 0 for all n ∈ N.

Русский

Аннигилятор подмодуля N состоит из скаляров, которые уничтожают весь N; то есть r ∈ Ann_R(N) тогда и только тогда, когда r·n = 0 для всех n ∈ N.

LaTeX

$$$ r \\in N.annihilator \\iff \\forall n \\in N,\; r \\cdot n = 0. $$$

Lean4

theorem le_annihilator_iff {N : Submodule R M} {I : Ideal R} : I ≤ annihilator N ↔ I • N = ⊥ := by
  simp_rw [← le_bot_iff, smul_le, SetLike.le_def, mem_annihilator]; rfl

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