WithDim

WithDim is the type M which carrying the dimension d.

structure WithDim (d : Dimension) (M : Type) : Type

The type M carrying an instance of a dimension d.

• val : M

  The underlying value of M.

theorem WithDim.ext {d : Dimension} {M : Type} (x1 x2 : WithDim d M) (h : x1.val = x2.val) : x1 = x2

theorem WithDim.ext_iff {d : Dimension} {M : Type} {x1 x2 : WithDim d M} : x1 = x2 ↔ x1.val = x2.val

instance WithDim.instHasDim (d : Dimension) (M : Type) : HasDim (WithDim d M)

Equations

• WithDim.instHasDim d M = { d := d }

@[simp]

theorem WithDim.dim_apply (d : Dimension) (M : Type) : dim (WithDim d M) = d

instance WithDim.instMulActionNNReal (d : Dimension) (M : Type) [MulAction NNReal M] : MulAction NNReal (WithDim d M)

Equations

• WithDim.instMulActionNNReal d M = { smul := fun (a : NNReal) (m : WithDim d M) => { val := a • m.val }, one_smul := ⋯, mul_smul := ⋯ }

@[simp]

theorem WithDim.smul_val {d : Dimension} {M : Type} [MulAction NNReal M] (a : NNReal) (m : WithDim d M) : (a • m).val = a • m.val

instance WithDim.instHMulRealHMulDimension {d1 d2 : Dimension} : HMul (WithDim d1 ℝ) (WithDim d2 ℝ) (WithDim (d1 * d2) ℝ)

Equations

• WithDim.instHMulRealHMulDimension = { hMul := fun (m1 : WithDim d1 ℝ) (m2 : WithDim d2 ℝ) => { val := m1.val * m2.val } }

theorem WithDim.withDim_hMul_val {d1 d2 : Dimension} (m1 : WithDim d1 ℝ) (m2 : WithDim d2 ℝ) : (m1 * m2).val = m1.val * m2.val

instance WithDim.instDMulRealHMulDimension {d1 d2 : Dimension} : DMul (WithDim d1 ℝ) (WithDim d2 ℝ) (WithDim (d1 * d2) ℝ)

Equations

• WithDim.instDMulRealHMulDimension = { toHMul := WithDim.instHMulRealHMulDimension, mul_dim := ⋯ }

@[simp]

theorem WithDim.val_mul_eq_mul {d1 d2 : Dimension} (m1 : WithDim d1 ℝ) (m2 : WithDim d2 ℝ) : m1.val * m2.val = (m1 * m2).val

@[simp]

theorem WithDim.val_pow_two_eq_mul {d1 : Dimension} (m1 : WithDim d1 ℝ) : m1.val ^ 2 = (m1 * m1).val

@[simp]

theorem WithDim.scaleUnit_val_eq_scaleUnit_val {d : Dimension} (M : Type) [MulAction NNReal M] (u1 u2 : UnitChoices) (m1 m2 : WithDim d M) : (UnitDependent.scaleUnit u1 u2 m1).val = (UnitDependent.scaleUnit u1 u2 m2).val ↔ m1.val = m2.val

theorem WithDim.scaleUnit_val_eq_scaleUnit_val_of_dim_eq {d1 d2 : Dimension} {M : Type} [MulAction NNReal M] {u1 u2 : UnitChoices} {m1 : WithDim d1 M} {m2 : WithDim d2 M} (h : d1 = d2 := by ext <;> { simp; try ring }) : (UnitDependent.scaleUnit u1 u2 m1).val = (UnitDependent.scaleUnit u1 u2 m2).val ↔ m1.val = m2.val

theorem WithDim.scaleUnit_val {d : Dimension} (M : Type) [MulAction NNReal M] (u1 u2 : UnitChoices) (m1 : WithDim d M) : (UnitDependent.scaleUnit u1 u2 m1).val = (u1.dimScale u2) d • m1.val

Division

noncomputable instance WithDim.instHDivRealHMulDimensionInv (d1 d2 : Dimension) : HDiv (WithDim d1 ℝ) (WithDim d2 ℝ) (WithDim (d1 * d2⁻¹) ℝ)

Equations

• WithDim.instHDivRealHMulDimensionInv d1 d2 = { hDiv := fun (m1 : WithDim d1 ℝ) (m2 : WithDim d2 ℝ) => { val := m1.val / m2.val } }

@[simp]

theorem WithDim.val_div_val {d1 d2 : Dimension} (m1 : WithDim d1 ℝ) (m2 : WithDim d2 ℝ) : m1.val / m2.val = (m1 / m2).val

@[simp]

theorem WithDim.div_scaleUnit {d1 d2 : Dimension} (m1 : WithDim d1 ℝ) (m2 : WithDim d2 ℝ) (u1 u2 : UnitChoices) : UnitDependent.scaleUnit u1 u2 m1 / UnitDependent.scaleUnit u1 u2 m2 = UnitDependent.scaleUnit u1 u2 (m1 / m2)

@[simp]

theorem WithDim.scaleUnit_dim_eq_zero {d : Dimension} (m : WithDim d ℝ) (u1 u2 : UnitChoices) (h : d = 1 := by ext <;> { simp; try ring }) : UnitDependent.scaleUnit u1 u2 m = m

Casting

def WithDim.cast {d d2 : Dimension} {M : Type} (m : WithDim d M) (h : d = d2 := by ext <;> { simp; try ring }) : WithDim d2 M

The casting from WithDim d M to WithDim d2 M when d = d2.

Equations

• m.cast h = { val := m.val }

@[simp]

theorem WithDim.cast_refl {d : Dimension} {M : Type} (m : WithDim d M) : m.cast ⋯ = m

@[simp]

theorem WithDim.cast_scaleUnit {d d2 : Dimension} {M : Type} [MulAction NNReal M] (m : WithDim d M) (h : d = d2) (u1 u2 : UnitChoices) : (UnitDependent.scaleUnit u1 u2 m).cast h = UnitDependent.scaleUnit u1 u2 (m.cast h)