Commit 2021-10-27 17:47 c529711f
View on Github →refactor(*): rename fpow and gpow to zpow (#9989)
Historically, we had two notions of integer power, one on groups called gpow and the other one on fields called fpow. Since the introduction of div_inv_monoid and group_with_zero, these definitions have been merged into one, and the boundaries are not clear any more. We rename both of them to zpow, adding a subscript 0 to disambiguate lemma names when there is a collision, where the subscripted version is for groups with zeroes (as is already done for inv lemmas).
To limit the scope of the change. this PR does not rename gsmul to zsmul or gmultiples to zmultiples.