unit_mul_mem_iff_mem — Mathlib

English

If I is an ideal of a ring and y is a unit, then for all x the product yx belongs to I if and only if x belongs to I.

Русский

Пусть I — идеал кольца, y — единичный элемент. Тогда для любого x выполняется: yx ∈ I тогда и только тогда, когда x ∈ I.

LaTeX

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

Lean4

@[simp]
theorem unit_mul_mem_iff_mem {x y : α} (hy : IsUnit y) : y * x ∈ I ↔ x ∈ I :=
  by
  refine ⟨fun h => ?_, fun h => I.mul_mem_left y h⟩
  obtain ⟨y', hy'⟩ := hy.exists_left_inv
  have := I.mul_mem_left y' h
  rwa [← mul_assoc, hy', one_mul] at this

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