## Stream: maths

### Topic: Maps between zmod

#### Adam Topaz (Sep 01 2020 at 21:06):

What's the idiomatic way to write down the ring hom from zmod a to zmod b given a proof that b divides a?

#### Mario Carneiro (Sep 01 2020 at 21:06):

Isn't there a cast?

#### Kevin Buzzard (Sep 01 2020 at 21:07):

Yes there's a cast which is a ring hom somewhere

#### Adam Topaz (Sep 01 2020 at 21:08):

Ah, yes, it's cast_hom thanks :)

#### Mario Carneiro (Sep 01 2020 at 21:08):

it was recently involved in a scandal, but it's a good citizen if you know b divides a

#### Adam Topaz (Sep 01 2020 at 21:13):

Oof src#zmod.cast is indeed a scandal.

#### Kevin Buzzard (Sep 01 2020 at 21:20):

Mathematically random and really hard to prove anything about!

#### Adam Topaz (Sep 01 2020 at 21:41):

Would it be crazy to do something like this?

import data.zmod.basic

variables (n N : ℕ)

class divides (n N : ℕ) := (cond : n ∣ N)

def proj [divides n N] : zmod N →+* zmod n := zmod.cast_hom (divides.cond : n ∣ N) _


#### Adam Topaz (Sep 01 2020 at 21:41):

I don't want to feed in divisibility proofs all the time.

#### Kyle Miller (Sep 01 2020 at 21:43):

I think [fact (n ∣ N)] covers this sort of thing. It seems hard to know when it's appropriate to use it!

#### Adam Topaz (Sep 01 2020 at 22:01):

Cool. Although I'm surprised that mathlib doesn't have something like this:

example {a b c : ℕ} [fact (b ≤ c)] : fact (a^b  ∣ a^c) := sorry


#### Mario Carneiro (Sep 01 2020 at 22:03):

fact is exclusively for lightweight local typeclass inference. Global fact instances are banned because you could put literally anything in a fact and lean has to search through all instances in a very stupid way

#### Adam Topaz (Sep 01 2020 at 22:04):

I see. I'll just abuse the typeclass search in my own project then.

#### Mario Carneiro (Sep 01 2020 at 22:05):

You can use localized to set up largeish fact problems across several files

#### Mario Carneiro (Sep 01 2020 at 22:05):

basically fact is opt in

#### Adam Topaz (Sep 01 2020 at 22:09):

I've never made a localized thing before. Is this the right syntax?

def foo {a b c : ℕ} [fact (b ≤ c)] : fact (a^b ∣ a^c) := sorry
localized "attribute [instance] foo" in bar


Last updated: May 11 2021 at 16:22 UTC