Zulip Chat Archive
Stream: Is there code for X?
Topic: Duplicated pow lemmas
Yaël Dillies (Nov 02 2021 at 15:10):
What's the point of docs#nat.pow_le_pow_of_le_left and surrouding lemmas given that we have their generalization in algebra.group_power.order?
Yaël Dillies (Nov 02 2021 at 15:12):
Am I hitting the limit of Damiano's order refactor?
Johan Commelin (Nov 02 2021 at 17:16):
cc @Damiano Testa
Last updated: May 02 2025 at 03:31 UTC