Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - chore(diamonds): appropriate transparency levels for diamond checks #10910

Closed
wants to merge 5 commits into from
Closed

[Merged by Bors] - chore(diamonds): appropriate transparency levels for diamond checks #10910

Changes from 1 commit
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
8121363
changes
mattrobball Feb 24, 2024
14bffea
fix
mattrobball Feb 24, 2024
1e2a9f0
two instances not one
kbuzzard Feb 24, 2024
258702a
restore
mattrobball Feb 24, 2024
aef7267
check test
mattrobball Feb 24, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
two instances not one
  • Loading branch information
@kbuzzard
kbuzzard committed Feb 24, 2024
commit 1e2a9f03acefc66ac575ed464c9664a1f9081c92
2 changes: 1 addition & 1 deletion Mathlib/Data/ZMod/IntUnitsPower.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -57,7 +57,7 @@ Notably this is satisfied by `R ∈ {ℕ, ℤ, ZMod 2}`. -/
instance Int.instUnitsPow : Pow ℤˣ R where
pow u r := Additive.toMul (r • Additive.ofMul u)

-- The above instance forms no typeclass diamonds with the standard power operators
-- The above instances form no typeclass diamonds with the standard power operators
-- but we will need `reducible_and_instances` which currently fails #10906
example : Int.instUnitsPow = Monoid.toNatPow := rfl
example : Int.instUnitsPow = DivInvMonoid.Pow := rfl
Expand Down
Loading