mathlib
082665e8 - feat(group_theory/index): relindex_eq_zero_of_le_right (#10928)

Commit

4 years ago

feat(group_theory/index): relindex_eq_zero_of_le_right (#10928) If H has infinite index in K, then so does any L ≥ K.

Author

tb65536

Parents