English
Transfer IsScalarTower G H M to IsScalarTower G H Mˣ under suitable hypotheses; the scalar action lifts to Units M.
Русский
Переносить IsScalarTower G H M на IsScalarTower G H Mˣ при разумных предпосылках; действие скаляра поднимается на Units M.
LaTeX
$$$ [IsScalarTower G H M] \\Rightarrow IsScalarTower G H (Units M)$$$
Lean4
/-- Transfer `IsScalarTower G H M` to `IsScalarTower G H Mˣ`. -/
@[to_additive /-- Transfer `VAddAssocClass G H M` to `VAddAssocClass G H (AddUnits M)`. -/
]
instance isScalarTower' [SMul G H] [Group G] [Group H] [Monoid M] [MulAction G M] [SMulCommClass G M M] [MulAction H M]
[SMulCommClass H M M] [IsScalarTower G M M] [IsScalarTower H M M] [IsScalarTower G H M] : IsScalarTower G H Mˣ where
smul_assoc g h m := Units.ext <| smul_assoc g h (m : M)
