English
divRight g defines a measurable equivalence on G with toEquiv = Equiv.divRight g, measurable_toFun = measurability of divisibility, measurable_invFun = measurability of multiplication by g.
Русский
divRight g задаёт измеримое эквивалентности на G с toEquiv = Equiv.divRight g и соответствующими свойствами измеримости.
LaTeX
$$$\\text{divRight}[\\MeasurableMul G](g) : G \\simeq^\\mathrm{m} G\\;\\text{with }\\; toEquiv = \\mathrm{Equiv.divRight}(g),\\; \\text{measurable\_toFun} = \\text{measurable\_div\_const}'(g),\\; \\text{measurable\_invFun} = \\text{measurable\_mul\_const}(g)$$$
Lean4
/-- `equiv.divRight` as a `MeasurableEquiv`. -/
@[to_additive /-- `equiv.subRight` as a `MeasurableEquiv` -/
]
def divRight [MeasurableMul G] (g : G) : G ≃ᵐ G
where
toEquiv := Equiv.divRight g
measurable_toFun := measurable_div_const' g
measurable_invFun := measurable_mul_const g
