Commit 2022-03-22 14:24 6a55ba89

View on Github →

feat(algebra/subalgebra/basic): Missing scalar instances (#12874) Add missing scalar instances for submonoid, subsemiring, subring, subalgebra.

Estimated changes

Modified src/algebra/algebra/subalgebra/basic.lean

modified theorem subalgebra.smul_def

Modified src/group_theory/submonoid/operations.lean

modified theorem submonoid.smul_def

Modified src/ring_theory/subring/basic.lean

modified theorem subring.smul_def

Modified src/ring_theory/subsemiring/basic.lean

modified theorem subsemiring.smul_def