LeanChemicalTheories / dimensional_analysis.basic

source

@[class]

structure has_time (α : Type u) :

Type u

dec : decidable_eq α
time : α

Instances of this typeclass

system1.has_time

Instances of other typeclasses for has_time

has_time.has_sizeof_inst

source

@[class]

structure has_length (α : Type u) :

Type u

dec : decidable_eq α
length : α

Instances of this typeclass

system1.has_length

Instances of other typeclasses for has_length

has_length.has_sizeof_inst

source

@[class]

structure has_mass (α : Type u) :

Type u

dec : decidable_eq α
mass : α

Instances for has_mass

has_mass.has_sizeof_inst

source

@[class]

structure has_amount_of_substance (α : Type u) :

Type u

dec : decidable_eq α
amount_of_substance : α

Instances for has_amount_of_substance

has_amount_of_substance.has_sizeof_inst

source

@[class]

structure has_electric_current (α : Type u) :

Type u

dec : decidable_eq α
electric_current : α

Instances for has_electric_current

has_electric_current.has_sizeof_inst

source

@[class]

structure has_temperature (α : Type u) :

Type u

dec : decidable_eq α
temperature : α

Instances for has_temperature

has_temperature.has_sizeof_inst

source

@[class]

structure has_luminous_intensity (α : Type u) :

Type u

dec : decidable_eq α
luminous_intensity : α

Instances for has_luminous_intensity

has_luminous_intensity.has_sizeof_inst

source

def dimension (α : Type u) :

Type u

Equations

dimension α = (α → ℚ)

Instances for dimension

source

def dimension.dimensionless (α : Type u_1) :

dimension α

Equations

dimension.dimensionless α = λ (i : α), 0

source

@[protected, instance]

def dimension.has_one {α : Type u_1} :

has_one (dimension α)

Equations

dimension.has_one = {one := dimension.dimensionless α}

source

@[protected, instance]

def dimension.nonempty {α : Type u_1} :

nonempty (dimension α)

source

@[protected, instance]

noncomputable def dimension.decidable_eq (α : Type u_1) (a b : dimension α) :

decidable (a = b)

Equations

dimension.decidable_eq α a b = classical.prop_decidable (a = b)

source

@[protected]

noncomputable def dimension.add {α : Type u_1} :

dimension α → dimension α → dimension α

Equations

dimension.add = classical.epsilon (λ (f : dimension α → dimension α → dimension α), ∀ (a b : dimension α), a = b → f a b = a)

source

@[protected]

noncomputable def dimension.sub {α : Type u_1} :

dimension α → dimension α → dimension α

Equations

dimension.sub = classical.epsilon (λ (f : dimension α → dimension α → dimension α), ∀ (a b : dimension α), a = b → f a b = a)

source

@[protected]

def dimension.mul {α : Type u_1} :

dimension α → dimension α → dimension α

Equations

a.mul b = λ (i : α), a i + b i

source

@[protected]

def dimension.div {α : Type u_1} :

dimension α → dimension α → dimension α

Equations

a.div b = λ (i : α), a i - b i

source

@[protected]

def dimension.qpow {α : Type u_1} :

dimension α → ℚ → dimension α

Equations

a.qpow n = λ (i : α), n • a i

source

@[protected]

def dimension.npow {α : Type u_1} :

dimension α → ℕ → dimension α

Equations

a.npow n = a.qpow ↑n

source

@[protected]

def dimension.zpow {α : Type u_1} :

dimension α → ℤ → dimension α

Equations

a.zpow n = a.qpow ↑n

source

@[protected]

def dimension.inv {α : Type u_1} :

dimension α → dimension α

Equations

a.inv = a.zpow (-1)

source

@[protected]

def dimension.le {α : Type u_1} :

dimension α → dimension α → Prop

Equations

a.le b = ite (a = b) true false

source

@[protected]

def dimension.lt {α : Type u_1} :

dimension α → dimension α → Prop

Equations

a.lt b = ite (a = b) true false

source

@[protected, instance]

noncomputable def dimension.has_add {α : Type u_1} :

has_add (dimension α)

Equations

dimension.has_add = {add := dimension.add α}

source

@[protected, instance]

noncomputable def dimension.has_sub {α : Type u_1} :

has_sub (dimension α)

Equations

dimension.has_sub = {sub := dimension.sub α}

source

@[protected, instance]

def dimension.has_mul {α : Type u_1} :

has_mul (dimension α)

Equations

dimension.has_mul = {mul := dimension.mul α}

source

@[protected, instance]

def dimension.has_div {α : Type u_1} :

has_div (dimension α)

Equations

dimension.has_div = {div := dimension.div α}

source

@[protected, instance]

def dimension.nat.has_pow {α : Type u_1} :

has_pow (dimension α) ℕ

Equations

dimension.nat.has_pow = {pow := dimension.npow α}

source

@[protected, instance]

def dimension.int.has_pow {α : Type u_1} :

has_pow (dimension α) ℤ

Equations

dimension.int.has_pow = {pow := dimension.zpow α}

source

@[protected, instance]

def dimension.rat.has_pow {α : Type u_1} :

has_pow (dimension α) ℚ

Equations

dimension.rat.has_pow = {pow := dimension.qpow α}

source

@[protected, instance]

def dimension.has_inv {α : Type u_1} :

has_inv (dimension α)

Equations

dimension.has_inv = {inv := dimension.inv α}

source

@[protected, instance]

def dimension.has_lt {α : Type u_1} :

has_lt (dimension α)

Equations

dimension.has_lt = {lt := dimension.lt α}

source

@[protected, instance]

def dimension.has_le {α : Type u_1} :

has_le (dimension α)

Equations

dimension.has_le = {le := dimension.le α}

source

@[protected]

def dimension.derivative {α : Type u_1} (b : dimension α) :

dimension α → dimension α

Equations

b.derivative = λ (a : dimension α), a / b

source

@[protected]

def dimension.integral {α : Type u_1} (b : dimension α) :

dimension α → dimension α

Equations

b.integral = λ (a : dimension α), a * b

source

@[simp]

theorem dimension.add_def {α : Type u_1} (a b : dimension α) :

a.add b = a + b

source

@[simp]

theorem dimension.add_def' {α : Type u_1} (a : dimension α) :

a.add a = a

source

@[simp]

theorem dimension.add_def'' {α : Type u_1} (a : dimension α) :

a + a = a

source

@[simp]

theorem dimension.sub_def {α : Type u_1} (a b : dimension α) :

a.sub b = a - b

source

@[simp]

theorem dimension.sub_def' {α : Type u_1} (a : dimension α) :

a.sub a = a

source

@[simp]

theorem dimension.sub_def'' {α : Type u_1} (a : dimension α) :

a - a = a

source

@[simp]

theorem dimension.mul_def {α : Type u_1} (a b : dimension α) :

a.mul b = a * b

source

@[simp]

theorem dimension.mul_def' {α : Type u_1} (a b : dimension α) :

a * b = λ (i : α), a i + b i

source

@[simp]

theorem dimension.div_def {α : Type u_1} (a b : dimension α) :

a.div b = a / b

source

@[simp]

theorem dimension.div_def' {α : Type u_1} (a b : dimension α) :

a / b = λ (i : α), a i - b i

source

@[simp]

theorem dimension.qpow_def {α : Type u_1} (a : dimension α) (b : ℚ) :

a.qpow b = a ^ b

source

@[simp]

theorem dimension.qpow_def' {α : Type u_1} (a : dimension α) (b : ℚ) :

a ^ b = λ (i : α), b • a i

source

@[simp]

theorem dimension.pow_def {α : Type u_1} (a : dimension α) (b : ℕ) :

a.npow b = a ^ b

source

@[simp]

theorem dimension.pow_def' {α : Type u_1} (a : dimension α) (b : ℕ) :

a ^ b = λ (i : α), b • a i

source

@[simp]

theorem dimension.zpow_def {α : Type u_1} (a : dimension α) (b : ℤ) :

a.zpow b = a ^ b

source

@[simp]

theorem dimension.zpow_def' {α : Type u_1} (a : dimension α) (b : ℤ) :

a ^ b = λ (i : α), b • a i

source

@[simp]

theorem dimension.inv_def {α : Type u_1} (a : dimension α) :

a.inv = a⁻¹

source

@[simp]

theorem dimension.inv_def' {α : Type u_1} (a : dimension α) :

a⁻¹ = λ (i : α), (-1) • a i

source

@[simp]

theorem dimension.le_def {α : Type u_1} (a b : dimension α) :

a.le b ↔ a ≤ b

source

@[simp]

theorem dimension.le_def' {α : Type u_1} (a : dimension α) :

a ≤ a

source

@[simp]

theorem dimension.lt_def {α : Type u_1} (a b : dimension α) :

a.lt b ↔ a < b

source

@[simp]

theorem dimension.lt_def' {α : Type u_1} (a : dimension α) :

a < a

source

def dimension.length (α : Type u_1) [has_length α] :

dimension α

Equations

dimension.length α = pi.single (has_length.length α) 1

source

def dimension.time (α : Type u_1) [has_time α] :

dimension α

Equations

dimension.time α = pi.single (has_time.time α) 1

source

def dimension.mass (α : Type u_1) [has_mass α] :

dimension α

Equations

dimension.mass α = pi.single (has_mass.mass α) 1

source

def dimension.amount_of_substance (α : Type u_1) [has_amount_of_substance α] :

dimension α

Equations

dimension.amount_of_substance α = pi.single (has_amount_of_substance.amount_of_substance α) 1

source

def dimension.electric_current (α : Type u_1) [has_electric_current α] :

dimension α

Equations

dimension.electric_current α = pi.single (has_electric_current.electric_current α) 1

source

def dimension.temperature (α : Type u_1) [has_temperature α] :

dimension α

Equations

dimension.temperature α = pi.single (has_temperature.temperature α) 1

source

def dimension.luminous_intensity (α : Type u_1) [has_luminous_intensity α] :

dimension α

Equations

dimension.luminous_intensity α = pi.single (has_luminous_intensity.luminous_intensity α) 1

source

@[simp]

theorem dimension.one_eq_dimensionless {α : Type u_1} :

1 = dimension.dimensionless α

source

@[simp]

theorem dimension.dimensionless_def' {α : Type u_1} :

dimension.dimensionless α = λ (i : α), 0

source

@[simp]

theorem dimension.bit0_dimension_eq_dimension {α : Type u_1} (a : dimension α) :

bit0 a = a

source

@[simp]

theorem dimension.bit1_dimensionless_eq_dimensionless {α : Type u_1} :

bit1 (dimension.dimensionless α) = dimension.dimensionless α

source

@[protected]

theorem dimension.mul_comm {α : Type u_1} (a b : dimension α) :

a * b = b * a

source

@[protected]

theorem dimension.div_mul_comm {α : Type u_1} (a b c : dimension α) :

a / c * b = b / c * a

source

@[protected]

theorem dimension.mul_assoc {α : Type u_1} (a b c : dimension α) :

a * b * c = a * (b * c)

source

@[protected]

theorem dimension.mul_one {α : Type u_1} (a : dimension α) :

a * 1 = a

source

@[protected]

theorem dimension.one_mul {α : Type u_1} (a : dimension α) :

1 * a = a

source

@[protected]

theorem dimension.div_eq_mul_inv {α : Type u_1} (a b : dimension α) :

a / b = a * b⁻¹

source

@[protected]

theorem dimension.mul_left_inv {α : Type u_1} (a : dimension α) :

a⁻¹ * a = 1

source

@[protected]

theorem dimension.mul_right_inv {α : Type u_1} (a : dimension α) :

a * a⁻¹ = 1

source

@[protected, instance]

def dimension.comm_group {α : Type u_1} :

comm_group (dimension α)

Equations

dimension.comm_group = {mul := dimension.mul α, mul_assoc := _, one := dimension.dimensionless α, one_mul := _, mul_one := _, npow := npow_rec dimension.has_mul, npow_zero' := _, npow_succ' := _, inv := dimension.inv α, div := dimension.div α, div_eq_mul_inv := _, zpow := zpow_rec dimension.has_inv, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _, mul_comm := _}

source

def dimension.velocity (α : Type u_1) [has_length α] [has_time α] :

dimension α

Equations

dimension.velocity α = dimension.length α / dimension.time α

source

def dimension.acceleration (α : Type u_1) [has_length α] [has_time α] :

dimension α

Equations

dimension.acceleration α = dimension.length α / dimension.time α ^ 2

source

def dimension.force (α : Type u_1) [has_length α] [has_time α] [has_mass α] :

dimension α

Equations

dimension.force α = dimension.length α / dimension.time α ^ 2 * dimension.mass α

source

theorem dimension.accel_eq_vel_div_time {α : Type u_1} [has_length α] [has_time α] :

dimension.acceleration α = dimension.velocity α / dimension.time α

source

theorem dimension.force_eq_mass_mul_accel {α : Type u_1} [has_length α] [has_time α] [has_mass α] :

dimension.force α = dimension.mass α * dimension.acceleration α

source

inductive system1 :

Type

time : system1
length : system1

Instances for system1

source

@[protected, instance]

def system1.decidable_eq :

decidable_eq system1

Equations

system1.decidable_eq system1.length system1.length = decidable.is_true rfl
system1.decidable_eq system1.length system1.time = decidable.is_false system1.decidable_eq._main._proof_2
system1.decidable_eq system1.time system1.length = decidable.is_false system1.decidable_eq._main._proof_1
system1.decidable_eq system1.time system1.time = decidable.is_true rfl

source

@[protected, instance]

def system1.has_time :

has_time system1

Equations

system1.has_time = {dec := system1.decidable_eq, time := system1.time}

source

@[protected, instance]

def system1.has_length :

has_length system1

Equations

system1.has_length = {dec := system1.decidable_eq, length := system1.length}

source

theorem system1_length_to_has_length :

system1.length = has_length.length system1

source

theorem system1_time_to_has_time :

system1.time = has_time.time system1

source

@[protected]

def system1.repr :

system1 → string

Equations

system1.length.repr = "length"
system1.time.repr = "time"

source

@[protected, instance]

def system1.has_repr :

has_repr system1

Equations

system1.has_repr = {repr := system1.repr}

source

theorem system1.accel_eq_vel_div_time :

dimension.acceleration system1 = dimension.velocity system1 / dimension.time system1

scilib documentation

Dimension type classes #

Def of dimensions and its properties #

Definition of the base dimensions #

Other dimensions #

examples for personal understanding #