mathlib3
0ace32b7 - change def mean: positivity -> monotonicity

Commit

3 years ago

change def mean: positivity -> monotonicity

References

#16574 - feat (group_theory/amenable) : define amenable groups

Author

matthias567

matthias567

Parents

Loading