mul_unit_mem_iff_mem — Mathlib

English

If y is a unit, then multiplying on the right by y preserves ideal membership: x y ∈ I iff x ∈ I.

Русский

Если y является единицей, умножение справа на y сохраняет членство в идеале: x y ∈ I ⇔ x ∈ I.

LaTeX

$$$\forall I\; (I: \text{Ideal } \alpha) \; \forall x,y\; (hy: \operatorname{IsUnit} y) : x \cdot y \in I \iff x \in I.$$$

Lean4

@[simp]
theorem mul_unit_mem_iff_mem {x y : α} (hy : IsUnit y) : x * y ∈ I ↔ x ∈ I :=
  mul_comm y x ▸ unit_mul_mem_iff_mem I hy

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