Units.smul_def
theorem Units.smul_def :
∀ {M : Type u_3} {α : Type u_5} [inst : Monoid M] [inst_1 : SMul M α] (m : Mˣ) (a : α), m • a = ↑m • a
This theorem, `Units.smul_def`, states that for any type `M` that is a monoid and any type `α` that allows scalar multiplication by `M`, if we have a unit `m` of `M` and an element `a` of `α`, then the scalar multiplication of `a` by `m` (written as `m • a`) is equivalent to the scalar multiplication of `a` by the value of `m` (written as `↑m • a`). In other words, the scalar multiplication operation behaves the same way whether we consider `m` as a unit or as a value of the monoid `M`.
More concisely: For any monoid `M` and type `α` with scalar multiplication, and for any unit `m` in `M` and element `a` in `α`, `m • a` is equal to `↑m • a`.
|
Units.smul_inv
theorem Units.smul_inv :
∀ {G : Type u_1} {M : Type u_3} [inst : Group G] [inst_1 : Monoid M] [inst_2 : MulAction G M]
[inst_3 : SMulCommClass G M M] [inst_4 : IsScalarTower G M M] (g : G) (m : Mˣ), (g • m)⁻¹ = g⁻¹ • m⁻¹
This theorem, `Units.smul_inv`, states that for any group `G`, monoid `M`, and given that `M` is a `G`-module with scalar multiplication (`smul`) that commutes with `M`'s multiplication and forms a scalar tower, the inverse of the scalar multiplication of an element `g` from the group `G` and an invertible element `m` from the monoid `M` is equal to the scalar multiplication of the inverse of `g` and the inverse of `m`. In mathematical notation, we have `(g • m)⁻¹ = g⁻¹ • m⁻¹` for all `g` in `G` and `m` in `Mˣ`.
More concisely: For any group `G`, monoid `M` with commuting scalar multiplication `smul` forming a scalar tower, the inverse of the product of an element `g` from `G` and an invertible element `m` from `M` is equal to the product of the inverses, i.e., `(g • m)⁻¹ = g⁻¹ • m⁻¹`.
|