# Zulip Chat Archive

## Stream: general

### Topic: Correct way to set up an instance with non-class parameters

#### Paul Lezeau (Dec 18 2022 at 16:25):

I'm currently trying to prove the following theorem

```
import ring_theory.adjoin_root
open polynomial localization
variables {R S : Type*} [comm_ring R] [comm_ring S] [algebra R S]
[is_domain S] [is_integrally_closed R]
example (a : S) (ha : is_integral R a) : minpoly (fraction_ring R) (algebra_map S
(fraction_ring S) a) ∣ (map_ring_hom (algebra_map R (fraction_ring R)) (minpoly R a)) :=
sorry
```

but for the statement to work I need the instance `algebra (fraction_ring R ) (fraction_ring S)`

. I wasn't able to find it in mathlib so I've tried to make my own, which yields the following MWE:

```
import ring_theory.adjoin_root
open polynomial localization
variables {R S : Type*} [comm_ring R] [comm_ring S] [algebra R S]
[is_domain S]
noncomputable def frac_algebra_of_inj (h : function.injective (algebra_map R S)):
algebra (fraction_ring R) (fraction_ring S) :=
ring_hom.to_algebra (is_fraction_ring.map h)
noncomputable instance problematic_instance (h : function.injective (algebra_map R S)):
algebra (fraction_ring R) (fraction_ring S) :=
frac_algebra_of_inj h
#lint /- IMPOSSIBLE INSTANCES FOUND.
These instances have an argument that cannot be found during type-class resolution,
and therefore can never succeed. Either mark the arguments with square brackets
(if it is a class), or don't make it an instance. -/
```

Since this instance is wrong according to `lint`

, what should I do?

#### Eric Wieser (Dec 18 2022 at 16:28):

Change `h`

to a `fact`

#### Eric Wieser (Dec 18 2022 at 16:30):

But note that this instance *might* bad for reasons not found by the linter; it likely creates a diamond for the action of `fraction_ring R`

on `fraction_ring (fraction_ring R))`

#### Kevin Buzzard (Dec 18 2022 at 16:32):

If anyone ever creates `fraction_ring (fraction_ring R))`

then they deserve the pain.

#### Paul Lezeau (Dec 18 2022 at 16:37):

Eric Wieser said:

Change

`h`

to a`fact`

Ok thanks, I'll try that!

#### Paul Lezeau (Dec 18 2022 at 16:37):

Eric Wieser said:

But note that this instance

mightbad for reasons not found by the linter; it likely creates a diamond for the action of`fraction_ring R`

on`fraction_ring (fraction_ring R))`

Yeah I was planning on making it into a local attribute once I managed to get it work!

Last updated: Dec 20 2023 at 11:08 UTC