instance

Stream: general

[Kenny Lau]

algebra/module.lean:

instance range {f : β → γ} (hf : is_linear_map f) : is_submodule (set.range f) :=
by rw [← set.image_univ]; exact is_submodule.image hf

should this be an instance?

[Mario Carneiro]

no good, unless is_linear_map is a typeclass

[Kenny Lau]

what to do about it then

[Mario Carneiro]

fix it?

[Guy Leroy]

I'm struggling with instances, I have the error:
failed to synthesize type class instance for

a n : ℕ,
_inst_1 : pos_nat n,
em : coprime a n
⊢ decidable_eq (coprime a n → Π [_inst_1 : pos_nat n], units (zmod n))

How should I state the instance that would solve this?

[Patrick Massot]

You should give us more context, this goal is probably not what you actually want

[Mario Carneiro]

While I agree with patrick, I doubt that this is the right goal to solve, it is incidentally provable. Probably the missing piece is decidable (pos_nat n)

[Guy Leroy]

Thanks Patrick, you're right, I made a mistake when writing my goal and it's all fixed now.
I would still be curious as to what this instance actually means.
As for the context I wrote

have : (units_zmod_mk a n) ^ order_of (units_zmod_mk a n), from pow_order_of_eq_one (units_zmod_mk a n),

instead of

have  : (units_zmod_mk a n em) ^ order_of (units_zmod_mk a n em) = 1, from pow_order_of_eq_one (units_zmod_mk a n em),

and I have defined above

def units_zmod_mk (a n : ℕ ) (h : nat.coprime a n) [pos_nat n] : units (zmod n) :=
{
    val := a,
    inv := a⁻¹,
    val_inv := by rw [mul_inv_eq_gcd n a, coprime.gcd_eq_one h];dsimp;rw zero_add,
    inv_val := by rw [mul_comm, mul_inv_eq_gcd n a, coprime.gcd_eq_one h];dsimp;rw zero_add,
}

[Guy Leroy]

Okay thanks Mario

[Mario Carneiro]

I assume the decidable_eq goal is coming from order_of

[Guy Leroy]

Very well thanks, I'm slowly trying to get a grasp of instances