English
If the space has zero dimension, the volume form is the canonical form on the zero-dimensional space, equal to the standard alternating isomorphism.
Русский
Для пространства нуловой размерности объемная форма совпадает с канонической формой на нулеверном пространстве, равной стандартной чередующейся изоморфии.
LaTeX
$$$$ \text{volumeForm} = \operatorname{AlternatingMap\,constLinearEquivOfIsEmpty}(1) \quad\text{when } \dim E = 0. $$$$
Lean4
@[simp]
theorem volumeForm_zero_pos [_i : Fact (finrank ℝ E = 0)] :
Orientation.volumeForm (positiveOrientation : Orientation ℝ E (Fin 0)) =
AlternatingMap.constLinearEquivOfIsEmpty 1 :=
by simp [volumeForm, Or.by_cases]