structure Units.Conversion : Type

Affine conversion between units.

⚠️ Warning : Affine composition works when offset is zero or factor is 1 ie : abbrev Affinable (c1 c2 : Conversion) : Prop := (c1.factor = 1 ∧ c2.factor = 1) ∨ (c1.offset = 0 ∧ c2.offset = 0)

instance (c₁ c₂ : Conversion) : Decidable (Affinable c₁ c₂) := by infer_instance

But we can't eforce it in the instances below because there is no way to attach the proof to the standard typeclasses. We could attach it to Conversion but that would restrict it too much. Indeed, it would prevent converting from celsius to fahrenheit directly.

• factor : ℚ
• offset : ℚ
• factor_ne_zero : self.factor ≠ 0

theorem Units.Conversion.ext_iff {x y : Conversion} : x = y ↔ x.factor = y.factor ∧ x.offset = y.offset

theorem Units.Conversion.ext {x y : Conversion} (factor : x.factor = y.factor) (offset : x.offset = y.offset) : x = y

instance Units.instReprConversion : Repr Conversion

Equations

• Units.instReprConversion = { reprPrec := Units.instReprConversion.repr }

def Units.instReprConversion.repr : Conversion → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Units.instDecidableEqConversion : DecidableEq Conversion

Equations

• Units.instDecidableEqConversion = Units.instDecidableEqConversion.decEq

def Units.instDecidableEqConversion.decEq (x✝ x✝¹ : Conversion) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

def Units.instBEqConversion.beq : Conversion → Conversion → Bool

Equations

• One or more equations did not get rendered due to their size.
• Units.instBEqConversion.beq x✝¹ x✝ = false

instance Units.instBEqConversion : BEq Conversion

Equations

• Units.instBEqConversion = { beq := Units.instBEqConversion.beq }

class Units.HasConversion (μ : Type) : Type

• conversion (u : μ) : Conversion

def Units.𝒞 {μ : Type} [self : HasConversion μ] (u : μ) : Conversion

Alias of Units.HasConversion.conversion.

Equations

• @Units.𝒞 = @Units.HasConversion.conversion

def Units.Conversion.identity : Conversion

Equations

• Units.Conversion.identity = { factor := 1, offset := 0, factor_ne_zero := Units.Conversion.identity._proof_1 }

instance Units.Conversion.instInhabited : Inhabited Conversion

Equations

• Units.Conversion.instInhabited = { default := Units.Conversion.identity }

def Units.Conversion.scale (s : ℚ) (h : s ≠ 0 := by simp) : Conversion

Equations

• Units.Conversion.scale s h = { factor := s, offset := 0, factor_ne_zero := h }

def Units.Conversion.translate (t : ℚ) : Conversion

Equations

• Units.Conversion.translate t = { factor := 1, offset := t, factor_ne_zero := Units.Conversion.identity._proof_1 }

def Units.Conversion.Scalable (c : Conversion) : Prop

Equations

• c.Scalable = (c.offset = 0)

instance Units.Conversion.instDecidableScalable (c : Conversion) : Decidable c.Scalable

Equations

• c.instDecidableScalable = id inferInstance

def Units.Conversion.mul (c1 c2 : Conversion) : Conversion

Equations

• c1.mul c2 = { factor := c1.factor * c2.factor, offset := c1.offset * c2.factor + c2.offset, factor_ne_zero := ⋯ }

def Units.Conversion.inv (c : Conversion) : Conversion

Equations

• c.inv = { factor := 1 / c.factor, offset := -c.offset / c.factor, factor_ne_zero := ⋯ }

def Units.Conversion.div (c1 c2 : Conversion) : Conversion

Equations

• c1.div c2 = c1.mul c2.inv

instance Units.Conversion.instMul : Mul Conversion

Equations

• Units.Conversion.instMul = { mul := Units.Conversion.mul }

instance Units.Conversion.instDiv : Div Conversion

Equations

• Units.Conversion.instDiv = { div := Units.Conversion.div }

instance Units.Conversion.instInv : Inv Conversion

Equations

• Units.Conversion.instInv = { inv := Units.Conversion.inv }

theorem Units.Conversion.mul_def (c1 c2 : Conversion) : c1 * c2 = c1.mul c2

theorem Units.Conversion.inv_def (c : Conversion) : c⁻¹ = c.inv

theorem Units.Conversion.div_def (c1 c2 : Conversion) : c1 / c2 = c1.mul c2.inv

def Units.Conversion.apply {α : Type u_1} [RatCast α] [Mul α] [Add α] (c : Conversion) (x : α) : α

Apply the conversion to a value x

Equations

• c.apply x = x * ↑c.factor + ↑c.offset

def Units.Conversion.convert {α : Type u_1} [RatCast α] [Mul α] [Add α] (c1 c2 : Conversion) (x : α) : α

Convert x from c1 to c2

Equations

• c1.convert c2 x = (c1 / c2).apply x

def Units.Conversion.add (c1 c2 : Conversion) : Conversion

Equations

• c1.add c2 = { factor := c1.factor * c2.factor, offset := c1.offset + c2.offset, factor_ne_zero := ⋯ }

def Units.Conversion.neg (c : Conversion) : Conversion

Equations

• c.neg = { factor := 1 / c.factor, offset := -c.offset, factor_ne_zero := ⋯ }

def Units.Conversion.sub (c1 c2 : Conversion) : Conversion

Equations

• c1.sub c2 = { factor := c1.factor / c2.factor, offset := c1.offset - c2.offset, factor_ne_zero := ⋯ }

def Units.Conversion.nsmul (s : ℕ) (c : Conversion) : Conversion

Equations

• Units.Conversion.nsmul s c = { factor := c.factor ^ s, offset := ↑s * c.offset, factor_ne_zero := ⋯ }

def Units.Conversion.zsmul (s : ℤ) (c : Conversion) : Conversion

Equations

• Units.Conversion.zsmul s c = { factor := c.factor ^ s, offset := ↑s * c.offset, factor_ne_zero := ⋯ }

instance Units.Conversion.instNeg : Neg Conversion

Equations

• Units.Conversion.instNeg = { neg := fun (c : Units.Conversion) => c.neg }

instance Units.Conversion.instZero : Zero Conversion

Equations

• Units.Conversion.instZero = { zero := Units.Conversion.identity }

instance Units.Conversion.instAdd : Add Conversion

Equations

• Units.Conversion.instAdd = { add := Units.Conversion.add }

instance Units.Conversion.instSub : Sub Conversion

Equations

• Units.Conversion.instSub = { sub := Units.Conversion.sub }

instance Units.Conversion.instSMulNat : SMul ℕ Conversion

Equations

• Units.Conversion.instSMulNat = { smul := Units.Conversion.nsmul }

instance Units.Conversion.instSMulInt : SMul ℤ Conversion

Equations

• Units.Conversion.instSMulInt = { smul := Units.Conversion.zsmul }

theorem Units.Conversion.zero_add' (c : Conversion) : identity.add c = c

theorem Units.Conversion.zero_add (c : Conversion) : 0 + c = c

theorem Units.Conversion.add_zero' (c : Conversion) : c.add identity = c

theorem Units.Conversion.add_zero (c : Conversion) : c + 0 = c

theorem Units.Conversion.add_comm' (c1 c2 : Conversion) : c1.add c2 = c2.add c1

theorem Units.Conversion.add_comm (c1 c2 : Conversion) : c1 + c2 = c2 + c1

theorem Units.Conversion.add_assoc' (c1 c2 c3 : Conversion) : (c1.add c2).add c3 = c1.add (c2.add c3)

theorem Units.Conversion.add_assoc (c1 c2 c3 : Conversion) : c1 + c2 + c3 = c1 + (c2 + c3)

theorem Units.Conversion.neg_add_cancel' (c : Conversion) : c.neg.add c = identity

theorem Units.Conversion.neg_add_cancel (c : Conversion) : -c + c = 0

theorem Units.Conversion.nsmul_zero (c : Conversion) : nsmul 0 c = identity

theorem Units.Conversion.nsmul_succ (s : ℕ) (c : Conversion) : nsmul (s + 1) c = (nsmul s c).add c

theorem Units.Conversion.sub_eq_add_neg' (c1 c2 : Conversion) : c1.sub c2 = c1.add c2.neg

theorem Units.Conversion.sub_eq_add_neg (c1 c2 : Conversion) : c1 - c2 = c1 + c2.neg

theorem Units.Conversion.zsmul_zero' (c : Conversion) : zsmul 0 c = identity

theorem Units.Conversion.zsmul_add_one (s : ℤ) (c : Conversion) : zsmul (s + 1) c = (zsmul s c).add c

theorem Units.Conversion.zsmul_succ' (n : ℕ) (c : Conversion) : zsmul (↑n.succ) c = zsmul (↑n) c + c

theorem Units.Conversion.zsmul_neg' (n : ℕ) (c : Conversion) : zsmul (Int.negSucc n) c = (zsmul (↑n.succ) c).neg

instance Units.Conversion.instAddCommGroup : AddCommGroup Conversion

Equations

• One or more equations did not get rendered due to their size.

theorem Units.Conversion.zero_div_zero : 0 / 0 = 0