toSphere_eq_zero_iff — Mathlib

English

For a Haar measure μ on a finite-dimensional real vector space E, μ.toSphere = 0 if and only if the dimension of E is zero.

Русский

Для меры Хаара μ на конечномерном вещественном пространстве E, μ.toSphere = 0 тогда и только тогда dim E = 0.

LaTeX

$$$\\mu.toSphere = 0 \\iff \\dim E = 0$$$

Lean4

theorem toSphere_eq_zero_iff : μ.toSphere = 0 ↔ Subsingleton E :=
  μ.toSphere_eq_zero_iff_finrank.trans Module.finrank_zero_iff

Похожие утверждения