mem_smul_iff_inv_mul_mem — Mathlib

English

Submodules of an algebra form an idempotent semiring under addition and multiplication.

Русский

Подмодули над кольцом образуют идемпотентное полукольцо под сложение и умножение.

LaTeX

$$$\\text{IdemSemiring}(\\mathrm{Submodule}\\; R\\; A)$$$

Lean4

theorem mem_smul_iff_inv_mul_mem {S} [DivisionSemiring S] [Algebra R S] {x : S} {p : Submodule R S} {y : S}
    (hx : x ≠ 0) : y ∈ x • p ↔ x⁻¹ * y ∈ p := by
  constructor
  · rintro ⟨a, ha : a ∈ p, rfl⟩; simpa [inv_mul_cancel_left₀ hx]
  · exact fun h ↦ ⟨_, h, by simp [mul_inv_cancel_left₀ hx]⟩

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