Division by 2

Definitions

class Div2 (α : Sort u_1) : Sort (max 1 u_1)

Division by 2

• div2 : α → α

class Div2Zero (α : Type u_1) [Zero α] [Div2 α] : Prop

Division by 2 respects zero

• div2_zero : div2 0 = 0

class ApproxDiv2 (α α' : Type) [Approx α α'] [Div2 α] [Div2 α'] : Prop

Division by 2 is conservative

• approx_div2 {x : α} {x' : α'} (a : approx x x') : approx (div2 x) (div2 x')

Modules over the rationals

Including the rationals themselves!

instance instDiv2OfSMulZeroClassRat {E : Type} [Zero E] [SMulZeroClass ℚ E] : Div2 E

Division by 2 for modules

Equations

• instDiv2OfSMulZeroClassRat = { div2 := fun (x : E) => 2⁻¹ • x }

instance instDiv2Zero {E : Type} [Zero E] [SMulZeroClass ℚ E] : Div2Zero E

Division by 2 respects zero for modules

theorem div2_eq_smul {E : Type} [Zero E] [SMulZeroClass ℚ E] (x : E) : div2 x = 2⁻¹ • x

theorem div2_eq_mul {𝕜 : Type} [Field 𝕜] [CharZero 𝕜] (x : 𝕜) : div2 x = 2⁻¹ * x