instance sphericalFiniteProperty_of_isEmpty {B : Type u_1} [DecidableEq B] [Fintype B] [IsEmpty B] (M : CoxeterMatrix B) : SphericalFiniteProperty M

The empty Coxeter matrix (no simple reflections) yields the trivial group, which is spherical and finite. This is the base case of the SphericalFiniteProperty typeclass.

instance sphericalFiniteProperty_A0 : SphericalFiniteProperty (CoxeterMatrix.A 0)

The trivial Coxeter type $A_0$ is spherical and finite (zero generators).