English
In an abelian group every left-invariant measure is also right-invariant.
Русский
В абелевой группе любая левая инвариантная мера также является правой инвариантной.
LaTeX
$$$\text{IsMulLeftInvariant}(\mu) \land \text{G is abelian} \Rightarrow \text{IsMulRightInvariant}(\mu)$$$
Lean4
/-- In an abelian group every left invariant measure is also right-invariant.
We don't declare the converse as an instance, since that would loop type-class inference, and
we use `IsMulLeftInvariant` as the default hypothesis in abelian groups. -/
@[to_additive IsAddLeftInvariant.isAddRightInvariant /--
In an abelian additive group every left invariant measure is also right-invariant. We don't
declare the converse as an instance, since that would loop type-class inference, and we use
`IsAddLeftInvariant` as the default hypothesis in abelian groups. -/
]
instance (priority := 100) isMulRightInvariant {μ : Measure G} [IsMulLeftInvariant μ] : IsMulRightInvariant μ :=
⟨fun g => by simp_rw [mul_comm, map_mul_left_eq_self]⟩
