# Zulip Chat Archive

## Stream: general

### Topic: modp setoid

#### Johan Commelin (Jun 06 2019 at 00:58):

Can something like this be made to work?

namespace modp variables (α : Type*) [comm_ring α] (p : ℕ) (hp : nat.prime p) def rel : setoid α := submodule.quotient_rel (ideal.span ({p} : set α)) local attribute [instance] rel variables {α p} lemma pow_add (a b : α) : (a + b)^p ≈ a^p + b^p := _ end modp

#### Chris Hughes (Jun 06 2019 at 01:04):

Look at `add_pow_char`

in `algebra.char_p`

#### Chris Hughes (Jun 06 2019 at 01:05):

and use `quotient_ring.quotient`

instead of `submodule.quotient`

#### Chris Hughes (Jun 06 2019 at 01:06):

Or `ideal.quotient`

. I forget the name.

#### Johan Commelin (Jun 06 2019 at 01:06):

I guess I should clarify (-;

#### Johan Commelin (Jun 06 2019 at 01:06):

I want to use the relation.

#### Johan Commelin (Jun 06 2019 at 01:06):

Point is that I want to do some computations with `mv_polynomial`

s over the integers, modulo `p`

.

#### Johan Commelin (Jun 06 2019 at 01:06):

And using this relation would make for readable `calc`

proofs

#### Reid Barton (Jun 06 2019 at 01:07):

Can you use `mv_polynomial`

s over the integers modulo `p`

?

#### Chris Hughes (Jun 06 2019 at 01:07):

But isn't it easier to map everything into the quotient and use `equality`

?

#### Johan Commelin (Jun 06 2019 at 01:07):

Otherwise you'll have `ideal.quotient.mk (ideal.span ({p} : set (mv_polynomial int _))`

all over the place...

#### Chris Hughes (Jun 06 2019 at 01:07):

use notation

#### Johan Commelin (Jun 06 2019 at 01:08):

I guess I could define a local notation for that... but then the proof state is still ugly

#### Chris Hughes (Jun 06 2019 at 01:08):

I don't like the fact that we can't quotient mod p without things being ugly.

#### Reid Barton (Jun 06 2019 at 01:12):

I was hoping you could use `parameter`

but it doesn't seem to help

#### Johan Commelin (Jun 06 2019 at 01:12):

I would like to write

calc [mod p] foo = bar : blah ... = xyzzy : etc

#### Johan Commelin (Jun 06 2019 at 01:12):

And then coercions should take care of the rest

#### Reid Barton (Jun 06 2019 at 01:13):

You should at least be able to write `calc foo =[p]= bar : blah ... = xyzzy : etc`

using notation

#### Reid Barton (Jun 06 2019 at 01:14):

though at that point I guess you should just define notation which depends on `p`

#### Johan Commelin (Jun 06 2019 at 01:16):

Isn't that what you are doing in your example?

#### Johan Commelin (Jun 06 2019 at 06:33):

Is interactive `calc`

in core or in mathlib? I couldn't find it easily

#### Kevin Buzzard (Jun 06 2019 at 06:35):

Must be in core because it's in TPIL

#### Johan Commelin (Jun 06 2019 at 06:40):

Is that interactive `calc`

or term-mode `calc`

?

#### Reid Barton (Jun 06 2019 at 07:29):

I mean in a section you can define local notation which depends on a `variable`

, so you don't need to write this funny `=[p]=`

stuff.

#### Johan Commelin (Jun 06 2019 at 07:33):

I am currently experimenting with

notation x ` modᵢ ` I := ideal.quotient.mk I x notation x ` modₛ ` s := ideal.quotient.mk (ideal.span s) x notation x ` modₑ ` a := ideal.quotient.mk (ideal.span ({a})) x

#### Johan Commelin (Jun 06 2019 at 07:34):

This can probably be improved quite a bit, using priorities etc... but I've no idea what would be sensible.

#### Johan Commelin (Jun 06 2019 at 07:40):

namespace modp variables {α : Type*} [comm_ring α] {p : ℕ} (hp : nat.prime p) notation x ` modᵢ ` I := ideal.quotient.mk I x notation x ` modₛ ` s := ideal.quotient.mk (ideal.span s) x notation x ` modₑ ` a := ideal.quotient.mk (ideal.span ({a})) x include hp instance (h : ¬ is_unit (p : α)) : char_p (ideal.span ({p} : set α)).quotient p := ⟨begin intro n, have helper : ∀ m : ℕ, (m : (ideal.span ({p} : set α)).quotient) = ideal.quotient.mk (ideal.span ({p} : set α)) (m : α), { intro m, induction m with m ih, {refl}, simp [ih] }, split, { intro H, rw [helper, ideal.quotient.eq_zero_iff_mem, ideal.mem_span_singleton] at H, rcases H with ⟨c, hc⟩, cases nat.coprime_or_dvd_of_prime hp n with hn hn, swap, {exact hn}, have key := nat.gcd_eq_gcd_ab p n, delta nat.coprime at hn, rw hn at key, replace key := congr_arg (λ k : ℤ, (k : α)) key, simp only [int.cast_coe_nat, int.cast_add, int.coe_nat_zero, int.cast_mul, int.cast_one, int.coe_nat_succ, zero_add, hc] at key, rw [mul_assoc, ← mul_add] at key, exfalso, apply h, rw is_unit_iff_exists_inv, exact ⟨_, key.symm⟩ }, { rintro ⟨c, rfl⟩, apply eq_zero_of_zero_dvd, use p, rw [zero_mul, helper (p*c), ideal.quotient.eq_zero_iff_mem, nat.cast_mul], exact ideal.mul_mem_right _ (ideal.subset_span $ set.mem_singleton p) } end⟩ . example (a b : α) : ((a + b)^p modₑ (p : α)) = (a^p modₑ (p : α)) + (b^p modₑ (p : α)) := begin sorry end end modp

#### Johan Commelin (Jun 06 2019 at 07:42):

Does `simp`

see through notation?

#### Reid Barton (Jun 06 2019 at 07:47):

Everything sees through notation

Last updated: May 14 2021 at 12:18 UTC