feat: the root space of a Coxeter group and the bilinear form on it

[trivial1711]

Prepare to define the standard geometric representation of a Coxeter group by defining the root space and the bilinear form on it. Then prove some lemmas about the orthogonal reflections in the simple roots.

Co-authored-by: Johan Commelin [email protected]

---

• [x] depends on: #11436
• [x] depends on: #11465

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#11436~~
• leanprover-community/mathlib4#11465 By Dependent Issues (🤖). Happy coding!

[trivial1711]

I would like to give B →₀ ℝ the instances AddCommMonoid, OrderedCancelAddCommMonoid, and SMulPosMono for this file only. I don't want to make the instances global. However, I do use the order relations > in some of my theorem statements. What is the best way to do this? I tried using

local notation "V" => B →₀ ℝ

scoped instance : AddCommMonoid V := Finsupp.instAddCommMonoid
scoped instance : OrderedCancelAddCommMonoid V := Finsupp.orderedCancelAddCommMonoid
scoped instance : SMulPosMono ℝ V := Finsupp.instSMulPosMono

but this really, really upsets the linter in a way that I don't understand:

/- The `defLemma` linter reports:
INCORRECT DEF/LEMMA: -/
-- Mathlib.GroupTheory.Coxeter.StandardGeometricRepresentation
Error: ./././Mathlib/GroupTheory/Coxeter/StandardGeometricRepresentation.lean:389:1: error: CoxeterSystem.instSMulPosMonoRealFinsuppInstZeroRealToSMulInstZeroSmulZeroClassToSMulZeroClassToSMulWithZeroToMulZeroClassToNonUnitalNonAssocSemiringToNonUnitalNonAssocCommSemiringToNonUnitalNonAssocCommRingToNonUnitalCommRingToNonUnitalSeminormedCommRingToSeminormedCommRingNormedCommRingInstPreorderRealPreorder.{u_2} is a def, should be lemma/theorem

/- The `docBlame` linter reports:
DEFINITIONS ARE MISSING DOCUMENTATION STRINGS: -/
-- Mathlib.GroupTheory.Coxeter.StandardGeometricRepresentation
Error: ./././Mathlib/GroupTheory/Coxeter/StandardGeometricRepresentation.lean:110:1: error: Matrix.instAddCommMonoidFinsuppRealInstZeroReal.{u_1} definition missing documentation string
Error: ./././Mathlib/GroupTheory/Coxeter/StandardGeometricRepresentation.lean:387:1: error: CoxeterSystem.instAddCommMonoidFinsuppRealInstZeroReal.{u_2} definition missing documentation string
Error: ./././Mathlib/GroupTheory/Coxeter/StandardGeometricRepresentation.lean:388:1: error: CoxeterSystem.instOrderedCancelAddCommMonoidFinsuppRealInstZeroReal.{u_2} definition missing documentation string
Error: ./././Mathlib/GroupTheory/Coxeter/StandardGeometricRepresentation.lean:389:1: error: CoxeterSystem.instSMulPosMonoRealFinsuppInstZeroRealToSMulInstZeroSmulZeroClassToSMulZeroClassToSMulWithZeroToMulZeroClassToNonUnitalNonAssocSemiringToNonUnitalNonAssocCommSemiringToNonUnitalNonAssocCommRingToNonUnitalCommRingToNonUnitalSeminormedCommRingToSeminormedCommRingNormedCommRingInstPreorderRealPreorder.{u_2} definition missing documentation string
Error: The process '/usr/bin/env' failed with exit code 1