WithDim

WithDim is the type M which carrying the dimension d.

structure WithDim (d : Dimension) (M : Type) [MulAction NNReal M] : 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} [MulAction NNReal M] (x1 x2 : WithDim d M) (h : x1.val = x2.val) : x1 = x2

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

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.instCarriesDimension (d : Dimension) (M : Type) [inst : MulAction NNReal M] : CarriesDimension (WithDim d M)

Equations

• WithDim.instCarriesDimension d M = { toMulAction := WithDim.instMulActionNNReal d M, d := d }

@[simp]

theorem WithDim.carriesDimension_d (d : Dimension) (M : Type) [MulAction NNReal M] : CarriesDimension.d (WithDim d M) = d

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 } }

@[simp]

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 := ⋯ }