structure Units.Quantity {δ : Type} (dim : δ) (α : Type) [AddCommGroup δ] : Type

• val : α

def Units.instInhabitedQuantity.default {a✝ : Type} {a✝¹ : a✝} {a✝² : Type} [Inhabited a✝²] {a✝³ : AddCommGroup a✝} : Quantity a✝¹ a✝²

Equations

• Units.instInhabitedQuantity.default = { val := default }

instance Units.instInhabitedQuantity {a✝ : Type} {a✝¹ : a✝} {a✝² : Type} [Inhabited a✝²] {a✝³ : AddCommGroup a✝} : Inhabited (Quantity a✝¹ a✝²)

Equations

• Units.instInhabitedQuantity = { default := Units.instInhabitedQuantity.default }

instance Units.instBEqQuantity {δ✝ : Type} {dim✝ : δ✝} {α✝ : Type} {inst✝ : AddCommGroup δ✝} [BEq δ✝] [BEq α✝] : BEq (Quantity dim✝ α✝)

Equations

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

def Units.instBEqQuantity.beq {δ✝ : Type} {dim✝ : δ✝} {α✝ : Type} {inst✝ : AddCommGroup δ✝} [BEq δ✝] [BEq α✝] : Quantity dim✝ α✝ → Quantity dim✝ α✝ → Bool

Equations

• Units.instBEqQuantity.beq { val := a } { val := b } = (a == b)
• Units.instBEqQuantity.beq x✝¹ x✝ = false

def Units.instDecidableEqQuantity.decEq {δ✝ : Type} {dim✝ : δ✝} {α✝ : Type} {inst✝ : AddCommGroup δ✝} [DecidableEq δ✝] [DecidableEq α✝] (x✝ x✝¹ : Quantity dim✝ α✝) : Decidable (x✝ = x✝¹)

Equations

• Units.instDecidableEqQuantity.decEq { val := a } { val := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance Units.instDecidableEqQuantity {δ✝ : Type} {dim✝ : δ✝} {α✝ : Type} {inst✝ : AddCommGroup δ✝} [DecidableEq δ✝] [DecidableEq α✝] : DecidableEq (Quantity dim✝ α✝)

Equations

• Units.instDecidableEqQuantity = Units.instDecidableEqQuantity.decEq

instance Units.Quantity.instRepr {α δ : Type} [AddCommGroup δ] [Repr δ] {d : δ} [Repr α] : Repr (Quantity d α)

Equations

• Units.Quantity.instRepr = { reprPrec := fun (q : Units.Quantity d α) (x : ℕ) => Std.Format.text (toString (repr q.val) ++ toString " • " ++ toString (repr d)) }

instance Units.Quantity.instToStringOfRepr {α δ : Type} [AddCommGroup δ] [Repr δ] {d : δ} [Repr α] : ToString (Quantity d α)

Equations

• Units.Quantity.instToStringOfRepr = { toString := fun (q : Units.Quantity d α) => reprStr q }

instance Units.Quantity.instZero {α δ : Type} [AddCommGroup δ] {d : δ} [Zero α] : Zero (Quantity d α)

Equations

• Units.Quantity.instZero = { zero := { val := 0 } }

instance Units.Quantity.instOne {α δ : Type} [AddCommGroup δ] {d : δ} [One α] : One (Quantity d α)

Equations

• Units.Quantity.instOne = { one := { val := 1 } }

def Units.Quantity.add {α δ : Type} [AddCommGroup δ] {d : δ} [Add α] (q1 q2 : Quantity d α) : Quantity d α

Equations

• q1.add q2 = { val := q1.val + q2.val }

instance Units.Quantity.instAdd {α δ : Type} [AddCommGroup δ] {d : δ} [Add α] : Add (Quantity d α)

Equations

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

def Units.Quantity.sub {α δ : Type} [AddCommGroup δ] {d : δ} [Sub α] (q1 q2 : Quantity d α) : Quantity d α

Equations

• q1.sub q2 = { val := q1.val - q2.val }

instance Units.Quantity.instSub {α δ : Type} [AddCommGroup δ] {d : δ} [Sub α] : Sub (Quantity d α)

Equations

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

def Units.Quantity.neg {α δ : Type} [AddCommGroup δ] {d : δ} [Neg α] (q : Quantity d α) : Quantity d α

Equations

• q.neg = { val := -q.val }

instance Units.Quantity.instNeg {α δ : Type} [AddCommGroup δ] {d : δ} [Neg α] : Neg (Quantity d α)

Equations

• Units.Quantity.instNeg = { neg := Units.Quantity.neg }

def Units.Quantity.hMul {α δ : Type} [AddCommGroup δ] {d₁ d₂ : δ} [Mul α] (q1 : Quantity d₁ α) (q2 : Quantity d₂ α) : Quantity (d₁ + d₂) α

Equations

• q1.hMul q2 = { val := q1.val * q2.val }

instance Units.Quantity.instHMulHAddOfMul {α δ : Type} [AddCommGroup δ] {d₁ d₂ : δ} [Mul α] : HMul (Quantity d₁ α) (Quantity d₂ α) (Quantity (d₁ + d₂) α)

Equations

• Units.Quantity.instHMulHAddOfMul = { hMul := Units.Quantity.hMul }

def Units.Quantity.hDiv {α δ : Type} [AddCommGroup δ] {d₁ d₂ : δ} [Div α] (q1 : Quantity d₁ α) (q2 : Quantity d₂ α) : Quantity (d₁ - d₂) α

Equations

• q1.hDiv q2 = { val := q1.val / q2.val }

instance Units.Quantity.instHDivHSubOfDiv {α δ : Type} [AddCommGroup δ] {d₁ d₂ : δ} [Div α] : HDiv (Quantity d₁ α) (Quantity d₂ α) (Quantity (d₁ - d₂) α)

Equations

• Units.Quantity.instHDivHSubOfDiv = { hDiv := Units.Quantity.hDiv }

def Units.Quantity.smul {α δ : Type} [AddCommGroup δ] {d : δ} [SMul α α] (s : α) (q : Quantity d α) : Quantity d α

Equations

• Units.Quantity.smul s q = { val := s • q.val }

def Units.Quantity.nsmul {α δ : Type} [AddCommGroup δ] {d : δ} [SMul ℕ α] (n : ℕ) (q : Quantity d α) : Quantity d α

Equations

• Units.Quantity.nsmul n q = { val := n • q.val }

def Units.Quantity.zsmul {α δ : Type} [AddCommGroup δ] {d : δ} [SMul ℤ α] (n : ℤ) (q : Quantity d α) : Quantity d α

Equations

• Units.Quantity.zsmul n q = { val := n • q.val }

def Units.Quantity.qsmul {α δ : Type} [AddCommGroup δ] {d : δ} [SMul ℚ α] (n : ℚ) (q : Quantity d α) : Quantity d α

Equations

• Units.Quantity.qsmul n q = { val := n • q.val }

instance Units.Quantity.instSMul {α δ : Type} [AddCommGroup δ] {d : δ} [SMul α α] : SMul α (Quantity d α)

Equations

• Units.Quantity.instSMul = { smul := Units.Quantity.smul }

instance Units.Quantity.instSMulNat {α δ : Type} [AddCommGroup δ] {d : δ} [SMul ℕ α] : SMul ℕ (Quantity d α)

Equations

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

instance Units.Quantity.instSMulInt {α δ : Type} [AddCommGroup δ] {d : δ} [SMul ℤ α] : SMul ℤ (Quantity d α)

Equations

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

instance Units.Quantity.instSMulRat {α δ : Type} [AddCommGroup δ] {d : δ} [SMul ℚ α] : SMul ℚ (Quantity d α)

Equations

• Units.Quantity.instSMulRat = { smul := Units.Quantity.qsmul }

def Units.Quantity.npow {α δ : Type} [AddCommGroup δ] {d : δ} [Pow α ℕ] (q : Quantity d α) (n : ℕ) : Quantity (n • d) α

Equations

• q.npow n = { val := q.val ^ n }

def Units.Quantity.zpow {α δ : Type} [AddCommGroup δ] {d : δ} [Pow α ℤ] (q : Quantity d α) (n : ℤ) : Quantity (n • d) α

Equations

• q.zpow n = { val := q.val ^ n }

def Units.Quantity.qpow {α δ : Type} [AddCommGroup δ] {d : δ} [Pow α ℚ] [SMul ℚ δ] (q : Quantity d α) (n : ℚ) : Quantity (n • d) α

Equations

• q.qpow n = { val := q.val ^ n }

instance Units.Quantity.instDPowNatHSMulOfPow {α δ : Type} [AddCommGroup δ] {d : δ} [Pow α ℕ] : DPow (Quantity d α) ℕ fun (n : ℕ) => Quantity (n • d) α

Equations

• Units.Quantity.instDPowNatHSMulOfPow = { pow := Units.Quantity.npow }

instance Units.Quantity.instDPowIntHSMulOfPow {α δ : Type} [AddCommGroup δ] {d : δ} [Pow α ℤ] : DPow (Quantity d α) ℤ fun (n : ℤ) => Quantity (n • d) α

Equations

• Units.Quantity.instDPowIntHSMulOfPow = { pow := Units.Quantity.zpow }

instance Units.Quantity.instDPowRatHSMulOfPow {α δ : Type} [AddCommGroup δ] {d : δ} [Pow α ℚ] [SMul ℚ δ] : DPow (Quantity d α) ℚ fun (n : ℚ) => Quantity (n • d) α

Equations

• Units.Quantity.instDPowRatHSMulOfPow = { pow := Units.Quantity.qpow }

def Units.Quantity.inv {α δ : Type} [AddCommGroup δ] {d : δ} [Inv α] (q : Quantity d α) : Quantity (-d) α

Equations

• q⁻¹ = { val := q.val⁻¹ }

def Units.Quantity.fun_to_val {α δ : Type} [AddCommGroup δ] {d₁ d₂ : δ} (f : Quantity d₁ α → Quantity d₂ α) : α → α

Equations

• Units.Quantity.fun_to_val f x = (f { val := x }).val

noncomputable def Units.Quantity.deriv {α δ : Type} [AddCommGroup δ] {d₁ d₂ : δ} [NontriviallyNormedField α] (f : Quantity d₁ α → Quantity d₂ α) (x : Quantity d₁ α) : Quantity (d₂ - d₁) α

Equations

• Units.Quantity.deriv f x = { val := deriv (Units.Quantity.fun_to_val f) x.val }

noncomputable def Units.Quantity.integral {α δ : Type} [AddCommGroup δ] {d₁ d₂ : δ} [NormedAddCommGroup α] [NormedSpace ℝ α] [MeasurableSpace α] (f : Quantity d₁ α → Quantity d₂ α) (μ : MeasureTheory.Measure α) : Quantity (d₁ + d₂) α

Equations

• Units.Quantity.integral f μ = { val := MeasureTheory.integral μ (Units.Quantity.fun_to_val f) }

def Units.Quantity.lt {α δ : Type} [AddCommGroup δ] {d : δ} [LT α] (q1 q2 : Quantity d α) : Prop

Equations

• q1.lt q2 = (q1.val < q2.val)

instance Units.Quantity.instLT {α δ : Type} [AddCommGroup δ] {d : δ} [LT α] : LT (Quantity d α)

Equations

• Units.Quantity.instLT = { lt := Units.Quantity.lt }

def Units.Quantity.le {α δ : Type} [AddCommGroup δ] {d : δ} [LE α] (q1 q2 : Quantity d α) : Prop

Equations

• q1.le q2 = (q1.val ≤ q2.val)

instance Units.Quantity.instLE {α δ : Type} [AddCommGroup δ] {d : δ} [LE α] : LE (Quantity d α)

Equations

• Units.Quantity.instLE = { le := Units.Quantity.le }

def Units.Quantity.dimension {α δ : Type} [AddCommGroup δ] {d : δ} [HasDimension δ] : Quantity d α → Dimension

Equations

• x✝.dimension = Units.𝒟 d

def Units.Quantity.conversion {α δ : Type} [AddCommGroup δ] {d : δ} [HasConversion δ] : Quantity d α → Conversion

Equations

• x✝.conversion = Units.𝒞 d

def Units.Quantity.units {α δ : Type} [AddCommGroup δ] {d : δ} : Quantity d α → δ

Equations

• x✝.units = d

instance Units.Quantity.instHasDimension {α δ : Type} [AddCommGroup δ] {d : δ} [HasDimension δ] : HasDimension (Quantity d α)

Equations

• Units.Quantity.instHasDimension = { dimension := Units.Quantity.dimension }

instance Units.Quantity.instHasConversion {α δ : Type} [AddCommGroup δ] {d : δ} [HasConversion δ] : HasConversion (Quantity d α)

Equations

• Units.Quantity.instHasConversion = { conversion := Units.Quantity.conversion }

def Units.Quantity.cast {α δ : Type} [AddCommGroup δ] {d₁ d₂ : δ} [HasEquiv δ] (q : Quantity d₁ α) : autoParam (d₁ ≈ d₂) _auto✝ → Quantity d₂ α

Preferred notation for casting: write ↑x instead of cast x.

• Purpose: ↑x is equivalent to cast x and is the idiomatic, preferred syntax throughout this library. Please use this notation in new code and docs.
• Precedence: the operator has high priority and binds tightly; use parentheses when needed, e.g. ↑(f x) or (↑x).field.
• Typing the symbol: in Lean/VSCode, type \uparrow then space to get ↑.

Examples:

• let q' : Quantity β := ↑q -- preferred
• -- instead of: cast q

Equations

• (↑q) x✝ = { val := q.val }

def Units.Quantity.convert {α δ : Type} [AddCommGroup δ] {d₁ d₂ : δ} [RatCast α] [Mul α] [Add α] [HasDimension δ] [HasConversion δ] (q : Quantity d₁ α) : autoParam (𝒟 d₁ = 𝒟 d₂) _auto✝ → Quantity d₂ α

convert from one quantity to another of the same dimension

Preferred notation for convert: write q → instead of convert q.

• Purpose: q → is equivalent to convert q and is the idiomatic, preferred syntax throughout this library. Please use this notation in new code and docs.

Examples:

• let q' : Quantity d₂ α := q → -- preferred
• -- instead of: convert q

Equations

• (q→) x✝ = { val := (Units.𝒞 d₁).convert (Units.𝒞 d₂) q.val }

def Units.Quantity.into {α δ : Type} [AddCommGroup δ] {d : δ} [RatCast α] [Mul α] [Add α] [HasDimension δ] [HasConversion δ] (q : Quantity d α) (target : δ) : autoParam (𝒟 d = 𝒟 target) _auto✝ → Quantity target α

convert and cast in one step from one quantity to another of the same dimension the target is a unit

Examples: convert constant c from natural unit to meter per second: c.into (Unit.meter-Unit.second)

Equations

• q.into target x✝ = { val := (Units.𝒞 d).convert (Units.𝒞 target) q.val }

def Units.Quantity.as {α δ : Type} [AddCommGroup δ] {d₁ d₂ : δ} [RatCast α] [Mul α] [Add α] [HasDimension δ] [HasConversion δ] (q : Quantity d₁ α) : Quantity d₂ α → autoParam (𝒟 d₁ = 𝒟 d₂) _auto✝ → Quantity d₂ α

convert and cast in one step from one quantity to another of the same dimension the target is another quantity

Examples:

• let q' : Quantity (Unit.meter-Unit.second) Float := q.as (m/s)

Equations

• q.as x✝¹ x✝ = { val := (Units.𝒞 d₁).convert (Units.𝒞 d₂) q.val }

def Units.Quantity.«term↑_» : Lean.ParserDescr

Preferred notation for casting: write ↑x instead of cast x.

• Purpose: ↑x is equivalent to cast x and is the idiomatic, preferred syntax throughout this library. Please use this notation in new code and docs.
• Precedence: the operator has high priority and binds tightly; use parentheses when needed, e.g. ↑(f x) or (↑x).field.
• Typing the symbol: in Lean/VSCode, type \uparrow then space to get ↑.

Examples:

• let q' : Quantity β := ↑q -- preferred
• -- instead of: cast q

Equations

• Units.Quantity.«term↑_» = Lean.ParserDescr.node `Units.Quantity.«term↑_» 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "↑") (Lean.ParserDescr.cat `term 100))

def Units.Quantity.«term_→» : Lean.TrailingParserDescr

convert from one quantity to another of the same dimension

Preferred notation for convert: write q → instead of convert q.

• Purpose: q → is equivalent to convert q and is the idiomatic, preferred syntax throughout this library. Please use this notation in new code and docs.

Examples:

• let q' : Quantity d₂ α := q → -- preferred
• -- instead of: convert q

Equations

• Units.Quantity.«term_→» = Lean.ParserDescr.trailingNode `Units.Quantity.«term_→» 100 100 (Lean.ParserDescr.symbol "→")

def Units.Quantity.«term_²» : Lean.TrailingParserDescr

Equations

• Units.Quantity.«term_²» = Lean.ParserDescr.trailingNode `Units.Quantity.«term_²» 1024 1024 (Lean.ParserDescr.symbol "²")

def Units.Quantity.«term_³» : Lean.TrailingParserDescr

Equations

• Units.Quantity.«term_³» = Lean.ParserDescr.trailingNode `Units.Quantity.«term_³» 1024 1024 (Lean.ParserDescr.symbol "³")

def Units.Quantity.«term_⁴» : Lean.TrailingParserDescr

Equations

• Units.Quantity.«term_⁴» = Lean.ParserDescr.trailingNode `Units.Quantity.«term_⁴» 1024 1024 (Lean.ParserDescr.symbol "⁴")

def Units.Quantity.«term_⁵» : Lean.TrailingParserDescr

Equations

• Units.Quantity.«term_⁵» = Lean.ParserDescr.trailingNode `Units.Quantity.«term_⁵» 1024 1024 (Lean.ParserDescr.symbol "⁵")

def Units.Quantity.«term_⁶» : Lean.TrailingParserDescr

Equations

• Units.Quantity.«term_⁶» = Lean.ParserDescr.trailingNode `Units.Quantity.«term_⁶» 1024 1024 (Lean.ParserDescr.symbol "⁶")

def Units.Quantity.«term_⁷» : Lean.TrailingParserDescr

Equations

• Units.Quantity.«term_⁷» = Lean.ParserDescr.trailingNode `Units.Quantity.«term_⁷» 1024 1024 (Lean.ParserDescr.symbol "⁷")

def Units.Quantity.«term_⁸» : Lean.TrailingParserDescr

Equations

• Units.Quantity.«term_⁸» = Lean.ParserDescr.trailingNode `Units.Quantity.«term_⁸» 1024 1024 (Lean.ParserDescr.symbol "⁸")

def Units.Quantity.«term_⁹» : Lean.TrailingParserDescr

Equations

• Units.Quantity.«term_⁹» = Lean.ParserDescr.trailingNode `Units.Quantity.«term_⁹» 1024 1024 (Lean.ParserDescr.symbol "⁹")

def Units.Quantity.«term_⁻²» : Lean.TrailingParserDescr

Equations

• Units.Quantity.«term_⁻²» = Lean.ParserDescr.trailingNode `Units.Quantity.«term_⁻²» 1024 1024 (Lean.ParserDescr.symbol "⁻²")

def Units.Quantity.«term_⁻³» : Lean.TrailingParserDescr

Equations

• Units.Quantity.«term_⁻³» = Lean.ParserDescr.trailingNode `Units.Quantity.«term_⁻³» 1024 1024 (Lean.ParserDescr.symbol "⁻³")

def Units.Quantity.«term_⁻⁴» : Lean.TrailingParserDescr

Equations

• Units.Quantity.«term_⁻⁴» = Lean.ParserDescr.trailingNode `Units.Quantity.«term_⁻⁴» 1024 1024 (Lean.ParserDescr.symbol "⁻⁴")

def Units.Quantity.«term_⁻⁵» : Lean.TrailingParserDescr

Equations

• Units.Quantity.«term_⁻⁵» = Lean.ParserDescr.trailingNode `Units.Quantity.«term_⁻⁵» 1024 1024 (Lean.ParserDescr.symbol "⁻⁵")

def Units.Quantity.«term_⁻⁶» : Lean.TrailingParserDescr

Equations

• Units.Quantity.«term_⁻⁶» = Lean.ParserDescr.trailingNode `Units.Quantity.«term_⁻⁶» 1024 1024 (Lean.ParserDescr.symbol "⁻⁶")

def Units.Quantity.«term_⁻⁷» : Lean.TrailingParserDescr

Equations

• Units.Quantity.«term_⁻⁷» = Lean.ParserDescr.trailingNode `Units.Quantity.«term_⁻⁷» 1024 1024 (Lean.ParserDescr.symbol "⁻⁷")

def Units.Quantity.«term_⁻⁸» : Lean.TrailingParserDescr

Equations

• Units.Quantity.«term_⁻⁸» = Lean.ParserDescr.trailingNode `Units.Quantity.«term_⁻⁸» 1024 1024 (Lean.ParserDescr.symbol "⁻⁸")

def Units.Quantity.«term_⁻⁹» : Lean.TrailingParserDescr

Equations

• Units.Quantity.«term_⁻⁹» = Lean.ParserDescr.trailingNode `Units.Quantity.«term_⁻⁹» 1024 1024 (Lean.ParserDescr.symbol "⁻⁹")

def Units.Quantity.«term_⁻¹» : Lean.TrailingParserDescr

Equations

• Units.Quantity.«term_⁻¹» = Lean.ParserDescr.trailingNode `Units.Quantity.«term_⁻¹» 1024 1024 (Lean.ParserDescr.symbol "⁻¹")