# (Scalar) multiplication and (vector) addition as measurable equivalences #

In this file we define the following measurable equivalences:

`MeasurableEquiv.smul`

: if a group`G`

acts on`α`

by measurable maps, then each element`c : G`

defines a measurable automorphism of`α`

;`MeasurableEquiv.vadd`

: additive version of`MeasurableEquiv.smul`

;`MeasurableEquiv.smul₀`

: if a group with zero`G`

acts on`α`

by measurable maps, then each nonzero element`c : G`

defines a measurable automorphism of`α`

;`MeasurableEquiv.mulLeft`

: if`G`

is a group with measurable multiplication, then left multiplication by`g : G`

is a measurable automorphism of`G`

;`MeasurableEquiv.addLeft`

: additive version of`MeasurableEquiv.mulLeft`

;`MeasurableEquiv.mulRight`

: if`G`

is a group with measurable multiplication, then right multiplication by`g : G`

is a measurable automorphism of`G`

;`MeasurableEquiv.addRight`

: additive version of`MeasurableEquiv.mulRight`

;`MeasurableEquiv.mulLeft₀`

,`MeasurableEquiv.mulRight₀`

: versions of`MeasurableEquiv.mulLeft`

and`MeasurableEquiv.mulRight`

for groups with zero;`MeasurableEquiv.inv`

:`Inv.inv`

as a measurable automorphism of a group (or a group with zero);`MeasurableEquiv.neg`

: negation as a measurable automorphism of an additive group.

We also deduce that the corresponding maps are measurable embeddings.

## Tags #

measurable, equivalence, group action

If an additive group `G`

acts on `α`

by measurable maps, then each element `c : G`

defines a measurable automorphism of `α`

.

## Equations

- MeasurableEquiv.vadd c = { toEquiv := AddAction.toPerm c, measurable_toFun := ⋯, measurable_invFun := ⋯ }

## Instances For

If a group `G`

acts on `α`

by measurable maps, then each element `c : G`

defines a measurable
automorphism of `α`

.

## Equations

- MeasurableEquiv.smul c = { toEquiv := MulAction.toPerm c, measurable_toFun := ⋯, measurable_invFun := ⋯ }

## Instances For

If a group with zero `G₀`

acts on `α`

by measurable maps, then each nonzero element `c : G₀`

defines a measurable automorphism of `α`

## Equations

- MeasurableEquiv.smul₀ c hc = MeasurableEquiv.smul (Units.mk0 c hc)

## Instances For

If `G`

is an additive group with measurable addition, then addition of `g : G`

on the left is a measurable automorphism of `G`

.

## Equations

## Instances For

If `G`

is a group with measurable multiplication, then left multiplication by `g : G`

is a
measurable automorphism of `G`

.

## Equations

## Instances For

If `G`

is an additive group with measurable addition, then addition of `g : G`

on the right is a measurable automorphism of `G`

.

## Equations

- MeasurableEquiv.addRight g = { toEquiv := Equiv.addRight g, measurable_toFun := ⋯, measurable_invFun := ⋯ }

## Instances For

If `G`

is a group with measurable multiplication, then right multiplication by `g : G`

is a
measurable automorphism of `G`

.

## Equations

- MeasurableEquiv.mulRight g = { toEquiv := Equiv.mulRight g, measurable_toFun := ⋯, measurable_invFun := ⋯ }

## Instances For

If `G₀`

is a group with zero with measurable multiplication, then left multiplication by a
nonzero element `g : G₀`

is a measurable automorphism of `G₀`

.

## Equations

- MeasurableEquiv.mulLeft₀ g hg = MeasurableEquiv.smul₀ g hg

## Instances For

If `G₀`

is a group with zero with measurable multiplication, then right multiplication by a
nonzero element `g : G₀`

is a measurable automorphism of `G₀`

.

## Equations

- MeasurableEquiv.mulRight₀ g hg = { toEquiv := Equiv.mulRight₀ g hg, measurable_toFun := ⋯, measurable_invFun := ⋯ }

## Instances For

Negation as a measurable automorphism of an additive group.

## Equations

- MeasurableEquiv.neg G = { toEquiv := Equiv.neg G, measurable_toFun := ⋯, measurable_invFun := ⋯ }

## Instances For

Inversion as a measurable automorphism of a group or group with zero.

## Equations

- MeasurableEquiv.inv G = { toEquiv := Equiv.inv G, measurable_toFun := ⋯, measurable_invFun := ⋯ }

## Instances For

`equiv.subRight`

as a `MeasurableEquiv`

## Equations

- MeasurableEquiv.subRight g = { toEquiv := Equiv.subRight g, measurable_toFun := ⋯, measurable_invFun := ⋯ }

## Instances For

`equiv.divRight`

as a `MeasurableEquiv`

.

## Equations

- MeasurableEquiv.divRight g = { toEquiv := Equiv.divRight g, measurable_toFun := ⋯, measurable_invFun := ⋯ }

## Instances For

`equiv.subLeft`

as a `MeasurableEquiv`

## Equations

- MeasurableEquiv.subLeft g = { toEquiv := Equiv.subLeft g, measurable_toFun := ⋯, measurable_invFun := ⋯ }

## Instances For

`equiv.divLeft`

as a `MeasurableEquiv`

## Equations

- MeasurableEquiv.divLeft g = { toEquiv := Equiv.divLeft g, measurable_toFun := ⋯, measurable_invFun := ⋯ }