English
RingQuot r carries an algebra structure over S when R is an S-algebra and r is given.
Русский
RingQuot r обладает структурой алгебры над S, когда R — алгебра над S и задана эквивалентность.
LaTeX
$$$\text{Algebra}(S, \mathrm{Quot}(R,r))$$$
Lean4
instance instAlgebra [Algebra S R] (r : R → R → Prop) : Algebra S (RingQuot r)
where
smul := (· • ·)
algebraMap :=
{ toFun r := ⟨Quot.mk _ (algebraMap S R r)⟩
map_one' := by simp [← one_quot]
map_mul' := by simp [mul_quot]
map_zero' := by simp [← zero_quot]
map_add' := by simp [add_quot] }
commutes'
r := by
rintro ⟨⟨a⟩⟩
simp [Algebra.commutes, mul_quot]
smul_def'
r := by
rintro ⟨⟨a⟩⟩
simp [smul_quot, Algebra.smul_def, mul_quot]
