Scaling elements of WithTop

Left multiplication by c acts on WithTop α through WithTop.map (c * ·), fixing ⊤. This file records how this scaling interacts with WithTop.untop₀ and that scaling by a nonzero c in a group with zero is undone by scaling by c⁻¹.

Main results

• WithTop.untop₀_map_mul: (x.map (c * ·)).untop₀ = c * x.untop₀.
• WithTop.map_mul_map_inv_mul, WithTop.map_inv_mul_map_mul: scaling by c⁻¹ and by a nonzero c are mutually inverse.

@[simp]

theorem WithTop.untop₀_map_mul {α : Type u_1} [MulZeroClass α] (c : α) (x : WithTop α) : (map (fun (x : α) => c * x) x).untop₀ = c * x.untop₀

Scaling an element by a factor scales its real part; ⊤ keeps the real part zero.

theorem WithTop.map_mul_map_inv_mul {α : Type u_1} [GroupWithZero α] {c : α} (hc : c ≠ 0) (x : WithTop α) : map (fun (x : α) => c * x) (map (fun (x : α) => c⁻¹ * x) x) = x

Scaling an element by c⁻¹ and then by a nonzero c gives back the element.

theorem WithTop.map_inv_mul_map_mul {α : Type u_1} [GroupWithZero α] {c : α} (hc : c ≠ 0) (x : WithTop α) : map (fun (x : α) => c⁻¹ * x) (map (fun (x : α) => c * x) x) = x

Scaling an element by a nonzero c and then by c⁻¹ gives back the element.