Commit 2023-11-27 16:21 187f84fb

View on Github →

feat: remove an assumption (#8646) The assumption hn in finEquivZpowers_symm_apply always holds.

Estimated changes

modified theorem finEquivZpowers_symm_apply