structure SI_dimensions : Type

The SI unit system. In order to permit fractional dimensions, we allow dimensions to be rational; but then to maintain defeq of various explicit dimensions, we need to unseal the arithmetic operations on the rationals.

• units_length : ℚ
• units_mass : ℚ
• units_time : ℚ
• units_current : ℚ
• units_temperature : ℚ
• units_amount : ℚ
• units_intensity : ℚ

theorem SI_dimensions.ext {x y : SI_dimensions} (units_length : x.units_length = y.units_length) (units_mass : x.units_mass = y.units_mass) (units_time : x.units_time = y.units_time) (units_current : x.units_current = y.units_current) (units_temperature : x.units_temperature = y.units_temperature) (units_amount : x.units_amount = y.units_amount) (units_intensity : x.units_intensity = y.units_intensity) : x = y

theorem SI_dimensions.ext_iff {x y : SI_dimensions} : x = y ↔ x.units_length = y.units_length ∧ x.units_mass = y.units_mass ∧ x.units_time = y.units_time ∧ x.units_current = y.units_current ∧ x.units_temperature = y.units_temperature ∧ x.units_amount = y.units_amount ∧ x.units_intensity = y.units_intensity

instance instDecidableEqSI_dimensions : DecidableEq SI_dimensions

Equations

• instDecidableEqSI_dimensions = decEqSI_dimensions✝

instance SI_dimensions.instZero : Zero SI_dimensions

Equations

• SI_dimensions.instZero = { zero := { units_length := 0, units_mass := 0, units_time := 0, units_current := 0, units_temperature := 0, units_amount := 0, units_intensity := 0 } }

theorem SI_dimensions.zero_eq : 0 = { units_length := 0, units_mass := 0, units_time := 0, units_current := 0, units_temperature := 0, units_amount := 0, units_intensity := 0 }

instance SI_dimensions.instAdd : Add SI_dimensions

The addition structure here is simple enough that one gets a lot of definitional equalities, e.g., between d₁+d₂ and d₂+d₁ for explicit choices of d₁ and d₂, which is convenient as it means we do not need to utilize the cast operator much.

Equations

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

instance SI_dimensions.instNeg : Neg SI_dimensions

Equations

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

@[simp]

theorem Rat.neg_eq (q : ℚ) : q.neg = -q

theorem Rat.add_eq (q r : ℚ) : q.add r = q + r

instance SI_dimensions.instAddGroup : AddGroup SI_dimensions

Equations

• SI_dimensions.instAddGroup = AddGroup.ofLeftAxioms SI_dimensions.instAddGroup._proof_1 SI_dimensions.instAddGroup._proof_2 SI_dimensions.instAddGroup._proof_3

instance SI_dimensions.instAddCommGroup : AddCommGroup SI_dimensions

Equations

• SI_dimensions.instAddCommGroup = { toAddGroup := SI_dimensions.instAddGroup, add_comm := SI_dimensions.instAddCommGroup._proof_1 }

instance SI_dimensions.instSMul : SMul ℚ SI_dimensions

Equations

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

instance SI_dimensions.instModule : Module ℚ SI_dimensions

Equations

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

@[reducible, inline]

abbrev SI : UnitsSystem

Equations

• SI = { Dimensions := SI_dimensions, addCommGroup := SI_dimensions.instAddCommGroup }

instance instSI : UnitsSystem

The SI system will be automatically installed as a global instance by any Lean file that imports this one. This makes it difficult to use any competing unit system simultaneously, but that should be a rare use case.

Equations

• instSI = SI

instance instSI_module : Module ℚ UnitsSystem.Dimensions

Equations

• instSI_module = SI_dimensions.instModule

@[reducible, inline]

abbrev SI.deca {d : UnitsSystem.Dimensions} (q : UnitsSystem.Scalar d) : UnitsSystem.Scalar d

Equations

• SI.deca q = 10 • q

@[reducible, inline]

abbrev SI.hecto {d : UnitsSystem.Dimensions} (q : UnitsSystem.Scalar d) : UnitsSystem.Scalar d

Equations

• SI.hecto q = 10 ^ 2 • q

@[reducible, inline]

abbrev SI.kilo {d : UnitsSystem.Dimensions} (q : UnitsSystem.Scalar d) : UnitsSystem.Scalar d

Equations

• SI.kilo q = 10 ^ 3 • q

@[reducible, inline]

abbrev SI.mega {d : UnitsSystem.Dimensions} (q : UnitsSystem.Scalar d) : UnitsSystem.Scalar d

Equations

• SI.mega q = 10 ^ 6 • q

@[reducible, inline]

abbrev SI.giga {d : UnitsSystem.Dimensions} (q : UnitsSystem.Scalar d) : UnitsSystem.Scalar d

Equations

• SI.giga q = 10 ^ 9 • q

@[reducible, inline]

abbrev SI.tera {d : UnitsSystem.Dimensions} (q : UnitsSystem.Scalar d) : UnitsSystem.Scalar d

Equations

• SI.tera q = 10 ^ 12 • q

@[reducible, inline]

abbrev SI.peta {d : UnitsSystem.Dimensions} (q : UnitsSystem.Scalar d) : UnitsSystem.Scalar d

Equations

• SI.peta q = 10 ^ 15 • q

@[reducible, inline]

abbrev SI.exa {d : UnitsSystem.Dimensions} (q : UnitsSystem.Scalar d) : UnitsSystem.Scalar d

Equations

• SI.exa q = 10 ^ 18 • q

@[reducible, inline]

noncomputable abbrev SI.deci {d : UnitsSystem.Dimensions} (q : UnitsSystem.Scalar d) : UnitsSystem.Scalar d

Equations

• SI.deci q = 10 ^ (-1) • q

@[reducible, inline]

noncomputable abbrev SI.centi {d : UnitsSystem.Dimensions} (q : UnitsSystem.Scalar d) : UnitsSystem.Scalar d

Equations

• SI.centi q = 10 ^ (-2) • q

@[reducible, inline]

noncomputable abbrev SI.milli {d : UnitsSystem.Dimensions} (q : UnitsSystem.Scalar d) : UnitsSystem.Scalar d

Equations

• SI.milli q = 10 ^ (-3) • q

@[reducible, inline]

noncomputable abbrev SI.micro {d : UnitsSystem.Dimensions} (q : UnitsSystem.Scalar d) : UnitsSystem.Scalar d

Equations

• SI.micro q = 10 ^ (-6) • q

@[reducible, inline]

noncomputable abbrev SI.nano {d : UnitsSystem.Dimensions} (q : UnitsSystem.Scalar d) : UnitsSystem.Scalar d

Equations

• SI.nano q = 10 ^ (-9) • q

@[reducible, inline]

noncomputable abbrev SI.pico {d : UnitsSystem.Dimensions} (q : UnitsSystem.Scalar d) : UnitsSystem.Scalar d

Equations

• SI.pico q = 10 ^ (-12) • q

@[reducible, inline]

noncomputable abbrev SI.femto {d : UnitsSystem.Dimensions} (q : UnitsSystem.Scalar d) : UnitsSystem.Scalar d

Equations

• SI.femto q = 10 ^ (-15) • q

@[reducible, inline]

noncomputable abbrev SI.atto {d : UnitsSystem.Dimensions} (q : UnitsSystem.Scalar d) : UnitsSystem.Scalar d

Equations

• SI.atto q = 10 ^ (-18) • q

@[reducible, inline]

abbrev SI.Dimensionless : Type

Equations

• SI.Dimensionless = UnitsSystem.Scalar 0

@[reducible, inline]

abbrev SI.length_unit : UnitsSystem.Dimensions

Equations

• SI.length_unit = { units_length := 1, units_mass := 0, units_time := 0, units_current := 0, units_temperature := 0, units_amount := 0, units_intensity := 0 }

@[reducible, inline]

abbrev SI.Length : Type

Equations

• SI.Length = UnitsSystem.Scalar SI.length_unit

@[reducible, inline]

abbrev SI.meter : Length

Equations

• SI.meter = UnitsSystem.StandardUnit SI.length_unit

@[reducible, inline]

abbrev SI.mass_unit : UnitsSystem.Dimensions

Equations

• SI.mass_unit = { units_length := 0, units_mass := 1, units_time := 0, units_current := 0, units_temperature := 0, units_amount := 0, units_intensity := 0 }

@[reducible, inline]

abbrev SI.Mass : Type

Equations

• SI.Mass = UnitsSystem.Scalar SI.mass_unit

@[reducible, inline]

abbrev SI.kilogram : Mass

Equations

• SI.kilogram = UnitsSystem.StandardUnit SI.mass_unit

@[reducible, inline]

noncomputable abbrev SI.gram : Mass

Equations

• SI.gram = SI.milli SI.kilogram

@[reducible, inline]

abbrev SI.time_unit : UnitsSystem.Dimensions

Equations

• SI.time_unit = { units_length := 0, units_mass := 0, units_time := 1, units_current := 0, units_temperature := 0, units_amount := 0, units_intensity := 0 }

@[reducible, inline]

abbrev SI.Time : Type

Equations

• SI.Time = UnitsSystem.Scalar SI.time_unit

@[reducible, inline]

abbrev SI.second : Time

Equations

• SI.second = UnitsSystem.StandardUnit SI.time_unit

@[reducible, inline]

abbrev SI.minute : Time

Equations

• SI.minute = 60 • SI.second

@[reducible, inline]

abbrev SI.hour : Time

Equations

• SI.hour = 60 • SI.minute

@[reducible, inline]

abbrev SI.day : Time

Equations

• SI.day = 24 • SI.hour

@[reducible, inline]

abbrev SI.week : Time

Equations

• SI.week = 7 • SI.day

@[reducible, inline]

abbrev SI.year : Time

Equations

• SI.year = 365.25 • SI.day

@[reducible, inline]

abbrev SI.current_unit : UnitsSystem.Dimensions

Equations

• SI.current_unit = { units_length := 0, units_mass := 0, units_time := 0, units_current := 1, units_temperature := 0, units_amount := 0, units_intensity := 0 }

@[reducible, inline]

abbrev SI.Current : Type

Equations

• SI.Current = UnitsSystem.Scalar SI.current_unit

@[reducible, inline]

abbrev SI.ampere : Current

Equations

• SI.ampere = UnitsSystem.StandardUnit SI.current_unit

@[reducible, inline]

abbrev SI.temperature_unit : UnitsSystem.Dimensions

Equations

• SI.temperature_unit = { units_length := 0, units_mass := 0, units_time := 0, units_current := 0, units_temperature := 1, units_amount := 0, units_intensity := 0 }

@[reducible, inline]

abbrev SI.Temperature : Type

Equations

• SI.Temperature = UnitsSystem.Scalar SI.temperature_unit

@[reducible, inline]

abbrev SI.kelvin : Temperature

Equations

• SI.kelvin = UnitsSystem.StandardUnit SI.temperature_unit

@[reducible, inline]

abbrev SI.amount_unit : UnitsSystem.Dimensions

Equations

• SI.amount_unit = { units_length := 0, units_mass := 0, units_time := 0, units_current := 0, units_temperature := 0, units_amount := 1, units_intensity := 0 }

@[reducible, inline]

abbrev SI.Amount : Type

Equations

• SI.Amount = UnitsSystem.Scalar SI.amount_unit

@[reducible, inline]

abbrev SI.mole : Amount

Equations

• SI.mole = UnitsSystem.StandardUnit SI.amount_unit

@[reducible, inline]

abbrev SI.intensity_unit : UnitsSystem.Dimensions

Equations

• SI.intensity_unit = { units_length := 0, units_mass := 0, units_time := 0, units_current := 0, units_temperature := 0, units_amount := 0, units_intensity := 1 }

@[reducible, inline]

abbrev SI.Intensity : Type

Equations

• SI.Intensity = UnitsSystem.Scalar SI.intensity_unit

@[reducible, inline]

abbrev SI.candela : Intensity

Equations

• SI.candela = UnitsSystem.StandardUnit SI.intensity_unit

@[reducible, inline]

abbrev SI.speed_unit : UnitsSystem.Dimensions

Equations

• SI.speed_unit = SI.length_unit - SI.time_unit

@[reducible, inline]

abbrev SI.Speed : Type

Equations

• SI.Speed = UnitsSystem.Scalar SI.speed_unit

@[reducible, inline]

abbrev SI.acceleration_unit : UnitsSystem.Dimensions

Equations

• SI.acceleration_unit = SI.length_unit - 2 • SI.time_unit

@[reducible, inline]

abbrev SI.Acceleration : Type

Equations

• SI.Acceleration = UnitsSystem.Scalar SI.acceleration_unit

@[reducible, inline]

abbrev SI.momentum_unit : UnitsSystem.Dimensions

Equations

• SI.momentum_unit = SI.mass_unit + SI.speed_unit

@[reducible, inline]

abbrev SI.Momentum : Type

Equations

• SI.Momentum = UnitsSystem.Scalar SI.momentum_unit

@[reducible, inline]

abbrev SI.energy_unit : UnitsSystem.Dimensions

Equations

• SI.energy_unit = SI.mass_unit + 2 • SI.speed_unit

@[reducible, inline]

abbrev SI.Energy : Type

Equations

• SI.Energy = UnitsSystem.Scalar SI.energy_unit

@[reducible, inline]

abbrev SI.joule : Energy

Equations

• SI.joule = UnitsSystem.StandardUnit SI.energy_unit

@[reducible, inline]

abbrev SI.force_unit : UnitsSystem.Dimensions

Equations

• SI.force_unit = SI.mass_unit + SI.acceleration_unit

@[reducible, inline]

abbrev SI.Force : Type

Equations

• SI.Force = UnitsSystem.Scalar SI.force_unit

@[reducible, inline]

abbrev SI.newton : Force

Equations

• SI.newton = UnitsSystem.StandardUnit SI.force_unit

@[reducible, inline]

abbrev SI.frequency_unit : UnitsSystem.Dimensions

Equations

• SI.frequency_unit = -SI.time_unit

@[reducible, inline]

abbrev SI.Frequency : Type

Equations

• SI.Frequency = UnitsSystem.Scalar SI.frequency_unit

@[reducible, inline]

abbrev SI.hertz : Frequency

Equations

• SI.hertz = UnitsSystem.StandardUnit SI.frequency_unit

@[reducible, inline]

abbrev SI.pressure_unit : UnitsSystem.Dimensions

Equations

• SI.pressure_unit = SI.force_unit - 2 • SI.length_unit

@[reducible, inline]

abbrev SI.Pressure : Type

Equations

• SI.Pressure = UnitsSystem.Scalar SI.pressure_unit

@[reducible, inline]

abbrev SI.pascal : Pressure

Equations

• SI.pascal = UnitsSystem.StandardUnit SI.pressure_unit

@[reducible, inline]

abbrev SI.power_unit : UnitsSystem.Dimensions

Equations

• SI.power_unit = SI.energy_unit - SI.time_unit

@[reducible, inline]

abbrev SI.Power : Type

Equations

• SI.Power = UnitsSystem.Scalar SI.power_unit

@[reducible, inline]

abbrev SI.watt : Power

Equations

• SI.watt = UnitsSystem.StandardUnit SI.power_unit

@[reducible, inline]

abbrev SI.charge_unit : UnitsSystem.Dimensions

Equations

• SI.charge_unit = SI.current_unit + SI.time_unit

@[reducible, inline]

abbrev SI.Charge : Type

Equations

• SI.Charge = UnitsSystem.Scalar SI.charge_unit

@[reducible, inline]

abbrev SI.coulomb : Charge

Equations

• SI.coulomb = UnitsSystem.StandardUnit SI.charge_unit

@[reducible, inline]

abbrev SI.voltage_unit : UnitsSystem.Dimensions

Equations

• SI.voltage_unit = SI.energy_unit - SI.charge_unit

@[reducible, inline]

abbrev SI.Voltage : Type

Equations

• SI.Voltage = UnitsSystem.Scalar SI.voltage_unit

@[reducible, inline]

abbrev SI.volt : Voltage

Equations

• SI.volt = UnitsSystem.StandardUnit SI.voltage_unit

@[reducible, inline]

abbrev SI.capacitance_unit : UnitsSystem.Dimensions

Equations

• SI.capacitance_unit = SI.charge_unit - SI.voltage_unit

@[reducible, inline]

abbrev SI.Capacitance : Type

Equations

• SI.Capacitance = UnitsSystem.Scalar SI.capacitance_unit

@[reducible, inline]

abbrev SI.farad : Capacitance

Equations

• SI.farad = UnitsSystem.StandardUnit SI.capacitance_unit

@[reducible, inline]

abbrev SI.resistance_unit : UnitsSystem.Dimensions

Equations

• SI.resistance_unit = SI.voltage_unit - SI.current_unit

@[reducible, inline]

abbrev SI.Resistance : Type

Equations

• SI.Resistance = UnitsSystem.Scalar SI.resistance_unit

@[reducible, inline]

abbrev SI.ohm : Resistance

Equations

• SI.ohm = UnitsSystem.StandardUnit SI.resistance_unit

@[reducible, inline]

abbrev SI.inductance_unit : UnitsSystem.Dimensions

Equations

• SI.inductance_unit = SI.voltage_unit - 2 • SI.current_unit

@[reducible, inline]

abbrev SI.Inductance : Type

Equations

• SI.Inductance = UnitsSystem.Scalar SI.inductance_unit

@[reducible, inline]

abbrev SI.henry : Inductance

Equations

• SI.henry = UnitsSystem.StandardUnit SI.inductance_unit

@[reducible, inline]

abbrev SI.magnetic_flux_unit : UnitsSystem.Dimensions

Equations

• SI.magnetic_flux_unit = SI.voltage_unit + SI.time_unit

@[reducible, inline]

abbrev SI.MagneticFlux : Type

Equations

• SI.MagneticFlux = UnitsSystem.Scalar SI.magnetic_flux_unit

@[reducible, inline]

abbrev SI.weber : MagneticFlux

Equations

• SI.weber = UnitsSystem.StandardUnit SI.magnetic_flux_unit

@[reducible, inline]

abbrev SI.magnetic_flux_density_unit : UnitsSystem.Dimensions

Equations

• SI.magnetic_flux_density_unit = SI.magnetic_flux_unit - SI.length_unit

@[reducible, inline]

abbrev SI.MagneticFluxDensity : Type

Equations

• SI.MagneticFluxDensity = UnitsSystem.Scalar SI.magnetic_flux_density_unit

@[reducible, inline]

abbrev SI.tesla : MagneticFluxDensity

Equations

• SI.tesla = UnitsSystem.StandardUnit SI.magnetic_flux_density_unit

@[reducible, inline]

abbrev SI.c : Speed

Equations

• SI.c = 299792458 • UnitsSystem.StandardUnit SI.speed_unit

@[reducible, inline]

noncomputable abbrev SI.h : UnitsSystem.Scalar (energy_unit + time_unit)

Equations

• SI.h = (6.62607015 * 10 ^ (-34)) • UnitsSystem.StandardUnit (SI.energy_unit + SI.time_unit)

@[reducible, inline]

noncomputable abbrev SI.e : Charge

Equations

• SI.e = (1.602176634 * 10 ^ (-19)) • UnitsSystem.StandardUnit SI.charge_unit

@[reducible, inline]

noncomputable abbrev SI.ε₀ : Capacitance

Equations

• SI.ε₀ = (8.854187817 * 10 ^ (-12)) • UnitsSystem.StandardUnit SI.capacitance_unit

@[reducible, inline]

noncomputable abbrev SI.μ₀ : Inductance

Equations

• SI.μ₀ = (4 * Real.pi * 10 ^ (-7)) • UnitsSystem.StandardUnit SI.inductance_unit

@[reducible, inline]

noncomputable abbrev SI.g : Acceleration

Equations

• SI.g = 9.80665 • UnitsSystem.StandardUnit SI.acceleration_unit

@[reducible, inline]

noncomputable abbrev SI.k : UnitsSystem.Scalar (energy_unit + temperature_unit)

Equations

• SI.k = (1.380649 * 10 ^ (-23)) • UnitsSystem.StandardUnit (SI.energy_unit + SI.temperature_unit)

@[reducible, inline]

noncomputable abbrev SI.N_A : Amount

Equations

• SI.N_A = (6.02214076 * 10 ^ 23) • UnitsSystem.StandardUnit SI.amount_unit