English
From a type S that satisfies SubsemiringClass and SMulMemClass, one creates a Subalgebra whose carrier is the given set S; the resulting object is a bona fide subalgebra of A with closure under addition, multiplication, and contains the base algebra image of R.
Русский
Из типа S, удовлетворяющего SubsemiringClass и SMulMemClass, образуется подалгебра, носителем которого выступает заданное множество S; полученная структура является подалгеброй A, замкнутой по сложению, умножению и содержащей образ алгебраMap(R) в S.
LaTeX
$$$ \text{Let } S \text{ be a set with the structure of a SubsemiringClass and SMulMemClass. Then } S \text{ gives rise to a subalgebra } S \subseteq A \text{ with the usual operations.}$$$
Lean4
/-- The actual `Subalgebra` obtained from an element of a type satisfying `SubsemiringClass` and
`SMulMemClass`. -/
@[simps]
def ofClass {S R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A] [SetLike S A] [SubsemiringClass S A]
[SMulMemClass S R A] (s : S) : Subalgebra R A where
carrier := s
add_mem' := add_mem
zero_mem' := zero_mem _
mul_mem' := mul_mem
one_mem' := one_mem _
algebraMap_mem' r := Algebra.algebraMap_eq_smul_one (A := A) r ▸ SMulMemClass.smul_mem r (one_mem s)
