This was raised in the discussion of #18092 but has been around for a long time:
We currently have the Algebra R A typeclass for commutative algebras that carries an inclusion map algebraMap : R -> A. We can also express non-commutative algebras using a combination of other typeclasses, but then the inclusion becomes a derived definition (for example, as (· • 1)). For better defeqs, if not simply mirroring actual mathematical practice, we should instead have a typeclass for non-commutative algebras that carries the inclusion map.
And in turn we should try to generalize this to canonical inclusions of groups etc.
When this issue is resolved:, it should be possible to revert the following definitions:
This was raised in the discussion of #18092 but has been around for a long time:
We currently have the
Algebra R Atypeclass for commutative algebras that carries an inclusion mapalgebraMap : R -> A. We can also express non-commutative algebras using a combination of other typeclasses, but then the inclusion becomes a derived definition (for example, as(· • 1)). For better defeqs, if not simply mirroring actual mathematical practice, we should instead have a typeclass for non-commutative algebras that carries the inclusion map.And in turn we should try to generalize this to canonical inclusions of groups etc.
When this issue is resolved:, it should be possible to revert the following definitions:
1 : Submodule R Achanges back from(· • 1)toLinearMap.range (Algebra.linearMap R A). (See [Merged by Bors] - refactor: change the definition of1 : Submodule R Ato the range of(· • 1)#18092.)