We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 0230b35 commit 18c69b7Copy full SHA for 18c69b7
1 file changed
theories/SymGroup/Bruhat.v
@@ -41,8 +41,8 @@ Matrix sum of permutation matrices:
41
42
Bruhat Order:
43
44
-- [s <=B t] == [s] is smaller than [t] for the right weak order.
45
-- [s <B t] == [s] is strictly smaller than [t] for the right weak order.
+- [s <=B t] == [s] is smaller than [t] for the Bruhat order.
+- [s <B t] == [s] is strictly smaller than [t] for the Bruhat order.
46
47
***************************)
48
From HB Require Import structures.
0 commit comments