theorem Units.Unit.mul_eq_add (u1 u2 : Unit) : u1 * u2 = u1 + u2

theorem Units.Unit.div_eq_sub (u1 u2 : Unit) : u1 / u2 = u1 - u2

theorem Units.Unit.inv_eq_neg (u : Unit) : u⁻¹ = -u

theorem Units.Unit.zpow_eq_zsmul (u : Unit) (n : ℤ) : u ^ n = n • u

theorem Units.Unit.npow_eq_nsmul (u : Unit) (n : ℕ) : u ^ n = n • u

theorem Units.Unit.equiv_refl {u : Unit} : u ≈ u

theorem Units.Unit.equiv_symm {u1 u2 : Unit} (h : u1 ≈ u2) : u2 ≈ u1

theorem Units.Unit.equiv_trans {u1 u2 u3 : Unit} (h1 : u1 ≈ u2) (h2 : u2 ≈ u3) : u1 ≈ u3

theorem Units.Unit.base_unit_dim_eq_dim (d : Dimension) (s : String) : (defineUnit s d).dimension = d

theorem Units.Unit.base_unit_dim_eq_self' (d : Dimension) (s : String) : 𝒟 (defineUnit s d) = d

theorem Units.Unit.derived_unit_dim_eq_dim (u : Unit) (s : String) (c : Conversion) : (defineDerivedUnit s u c).dimension = u.dimension

theorem Units.Unit.derived_unit_dim_eq_self' (u : Unit) (s : String) (c : Conversion) : 𝒟 (defineDerivedUnit s u c) = 𝒟 u

theorem Units.Unit.add_unit_dim {u1 u2 : Unit} : (u1 + u2).dimension = u1.dimension + u2.dimension

theorem Units.Unit.sub_unit_dim {u1 u2 : Unit} : (u1 - u2).dimension = u1.dimension - u2.dimension

theorem Units.Unit.neg_unit_dim {u : Unit} : (-u).dimension = -u.dimension

theorem Units.Unit.nsmul_unit_dim (c : ℕ) (u : Unit) : (c • u).dimension = c • u.dimension

theorem Units.Unit.zsmul_unit_dim (c : ℤ) (u : Unit) : (c • u).dimension = c • u.dimension

theorem Units.Unit.base_unit_conv_eq_conv (d : Dimension) (s : String) : (defineUnit s d).conversion = 0

theorem Units.Unit.conv_zero_eq_conv_identity : Conversion.identity = 0

theorem Units.Unit.conv_div_zero (c : Conversion) : c.div 0 = c

theorem Units.Unit.derived_unit_conv_eq_conv (u : Unit) (s : String) (c : Conversion) : (defineDerivedUnit s u c).conversion = c / u.conversion

theorem Units.Unit.add_unit_conv {u1 u2 : Unit} : (u1 + u2).conversion = u1.conversion + u2.conversion

theorem Units.Unit.sub_unit_conv {u1 u2 : Unit} : (u1 - u2).conversion = u1.conversion - u2.conversion

theorem Units.Unit.neg_unit_conv {u : Unit} : (-u).conversion = -u.conversion

theorem Units.Unit.nsmul_unit_conv (c : ℕ) (u : Unit) : (c • u).conversion = c • u.conversion

theorem Units.Unit.zsmul_unit_conv (c : ℤ) (u : Unit) : (c • u).conversion = c • u.conversion