We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 86b4d32 commit fa54279Copy full SHA for fa54279
Mathlib/Data/ZMod/IntUnitsPower.lean
@@ -66,7 +66,7 @@ instance Int.instUnitsPow : Pow ℤˣ R where
66
-- The above instances form no typeclass diamonds with the standard power operators
67
-- but we will need `reducible_and_instances` which currently fails https://github.com/leanprover-community/mathlib4/issues/10906
68
example : Int.instUnitsPow = Monoid.toPow := rfl
69
-example : Int.instUnitsPow = DivInvMonoid.toZPow := rfl
+example : Int.instUnitsPow = DivInvMonoid.toPow := rfl
70
71
@[simp] lemma ofMul_uzpow (u : ℤˣ) (r : R) : Additive.ofMul (u ^ r) = r • Additive.ofMul u := rfl
72
0 commit comments