English
Let R be a commutative ring and A a nonunital R-algebra. The map that sends a NonUnitalSubalgebra S of A to its corresponding NonUnitalSubsemiring S.toNonUnitalSubsemiring is injective; i.e., if S.toNonUnitalSubsemiring = T.toNonUnitalSubsemiring then S = T.
Русский
Пусть R — коммутативное кольцо, и A — ненулевой R-алгебра. Отображение, переводящее подпольгалгебру S ⊆ A в соответствующую подполугруппу полугруппы S.toNonUnitalSubsemiring, инъективно: если S.toNonUnitalSubsemiring = T.toNonUnitalSubsemiring, то S = T.
LaTeX
$$$\forall S,U \in \text{NonUnitalSubalgebra}(R,A),\; S.toNonUnitalSubsemiring = U.toNonUnitalSubsemiring \Rightarrow S = U$$$
Lean4
theorem toNonUnitalSubsemiring_injective :
Function.Injective (toNonUnitalSubsemiring : NonUnitalSubalgebra R A → NonUnitalSubsemiring A) := fun S T h =>
ext fun x => by rw [← mem_toNonUnitalSubsemiring, ← mem_toNonUnitalSubsemiring, h]
