English
There is a CanLift mechanism turning a subset of A into a NonUnitalSubalgebra, provided closure under 0, addition, multiplication and smul by R holds.
Русский
Существует механизм CanLift, превращающий подмножество A в NonUnitalSubalgebra, если оно замкнуто по 0, сложению, умножению и умножению на скаляры R.
LaTeX
$$CanLift(Set A) (NonUnitalSubalgebra.instSetLike.coe) …$$
Lean4
/-- The actual `NonUnitalSubalgebra` obtained from an element of a type satisfying
`NonUnitalSubsemiringClass` and `SMulMemClass`. -/
@[simps]
def ofClass {S R A : Type*} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SetLike S A]
[NonUnitalSubsemiringClass S A] [SMulMemClass S R A] (s : S) : NonUnitalSubalgebra R A
where
carrier := s
add_mem' := add_mem
zero_mem' := zero_mem _
mul_mem' := mul_mem
smul_mem' := SMulMemClass.smul_mem
