mem_one' — Mathlib

English

The membership of an element in the unit of SubMulAction is equivalent to the existence of a preimage under algebraMap.

Русский

Принадлежность элементa единице SubMulAction эквивалентна существованию предобраза под algebraMap.

LaTeX

$$$x \\in (1 : SubMulAction R A) \\iff \\exists y, \\ algebraMap R A y = x$$$

Lean4

theorem mem_one' {x : A} : x ∈ (1 : SubMulAction R A) ↔ ∃ y, algebraMap R A y = x :=
  exists_congr fun r => by rw [algebraMap_eq_smul_one]

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