Skip to content

Commit

Permalink
test(instance_diamonds): verify that restrict_scalars produces no dia…
Browse files Browse the repository at this point in the history
…monds on the complex numbers (#12273)

There is already a comment on `complex.module` that indicates an intentional solution to this diamond.
  • Loading branch information
eric-wieser committed Feb 24, 2022
1 parent a0d2c43 commit 0840629
Showing 1 changed file with 3 additions and 0 deletions.
3 changes: 3 additions & 0 deletions test/instance_diamonds.lean
Expand Up @@ -21,6 +21,9 @@ example :
(sub_neg_monoid.has_scalar_int : has_scalar ℤ ℂ) = (complex.has_scalar : has_scalar ℤ ℂ) :=
rfl

example : restrict_scalars.module ℝ ℂ ℂ = complex.module := rfl
example : restrict_scalars.algebra ℝ ℂ ℂ = complex.algebra := rfl

example (α β : Type*) [add_monoid α] [add_monoid β] :
(prod.has_scalar : has_scalar ℕ (α × β)) = add_monoid.has_scalar_nat := rfl

Expand Down

0 comments on commit 0840629

Please sign in to comment.