CharP R 2 ↔ 1 + 1 = 0

Stream: Is there code for X?

[Violeta Hernández]

What it says in the title. Can I show a monoid has characteristic 2 just by showing 1 + 1 = 0?

[Yaël Dillies]

No, because it could have characteristic one

[Violeta Hernández]

...with the extra 0 ≠ 1 assumption

[Ruben Van de Velde]

import Mathlib

example  (R : Type u_6) [NonAssocRing R] (h1 : (1 : R) ≠ 0) (h2 : (1 : R) + 1 = 0) : CharP R 2 := by
  convert CharP.addOrderOf_one R
  symm
  rw [addOrderOf_eq_iff two_pos]
  constructor
  · simpa [one_add_one_eq_two] using h2
  · intro m hmr hml
    interval_cases m
    simpa

[Ruben Van de Velde]

interval_cases m can also be obtain rfl : m = 1 := by omega

[Violeta Hernández]

Thanks! It'd be really nice to have this PR'd

[Ruben Van de Velde]

Go ahead :)

[Violeta Hernández]

Wait, does this require a ring? Surely you could do this with an arbitrary AddMonoidWithOne

[Ruben Van de Velde]

docs#CharP.addOrderOf_one uses docs#Nat.smul_one_eq_cast , I haven't thought about whether that's avoidable

[Violeta Hernández]

It should be. By induction, if n is even then n = 0, otherwise n = 1. This follows from just the equations and the fact zero is neutral.

[Violeta Hernández]

(deleted)

[Violeta Hernández]

I'm having a bit of trouble proving this though, the API for Even and Odd seems very undercooked. Why would docs#Nat.even_add_one use ¬ Even n instead of Odd n? Why isn't there a Nat.odd_add_one?

[Yaël Dillies]

The ¬ Even n is an historical accident by this point. Please fix it. Nat.odd_add_one doesn't need to exist since we have docs#Odd.add_odd

[Violeta Hernández]

Why does docs#Nat.not_even_iff use the n % 2 = 1 spelling? This is so frustrating

[Yaël Dillies]

Please fix, please fix :pray:

[Violeta Hernández]

Will do

[Violeta Hernández]

Oh wait, you have a PR related to that, don't you?

[Violeta Hernández]

Might be better to wait until that's merged

[Yaël Dillies]

Yes, #16024. Currently maintainer-merge

[Violeta Hernández]

Yaël Dillies said:

Nat.odd_add_one doesn't need to exist since we have docs#Odd.add_odd

It's annoying that's not an iff though.

[Violeta Hernández]

Simp lemmas Even (n + 1) ↔ Odd n and Odd (n + 1) ↔ Even n would be really nice

[Yaël Dillies]

Feel free to add Odd.add_even_iff, Odd.add_odd_iff

[Johan Commelin]

Yaël Dillies said:

Yes, #16024. Currently maintainer-merge

borsified

[Violeta Hernández]

import Mathlib.Algebra.CharP.Defs

variable {R : Type*} [AddMonoidWithOne R]

theorem eq_zero_or_one_of_one_add_one (h : (1 : R) + 1 = 0) (n : ℕ):
    (Even n → (n : R) = 0) ∧ (Odd n → (n : R) = 1) := by
  induction n with
  | zero => simp
  | succ n IH =>
      rw [Nat.even_add_one, ← Nat.odd_iff_not_even, Nat.odd_add]
      simp only [Nat.cast_add, Nat.odd_iff_not_even.not, Nat.cast_one, Nat.not_even_one, iff_false,
        Decidable.not_not, add_left_eq_self]
      obtain hn | hn := Nat.even_or_odd n
      · simp [hn, IH.1 hn]
      · simpa [hn, Nat.odd_iff_not_even.1 hn, IH.2 hn] using h

theorem char_two_of_one_add_one (h₁ : (1 : R) ≠ 0) (h₂ : (1 : R) + 1 = 0) : CharP R 2 := by
  constructor
  intro n
  obtain hn | hn := Nat.even_or_odd n
  · simpa [hn.two_dvd] using (eq_zero_or_one_of_one_add_one h₂ n).1 hn
  · simp [hn.not_two_dvd_nat]
    rwa [(eq_zero_or_one_of_one_add_one h₂ n).2 hn]

[Violeta Hernández]

I've never felt more at "odds" with simp

[Ruben Van de Velde]

import Mathlib.Algebra.CharP.Defs

lemma Nat.odd_add_one {n : ℕ} : Odd (n + 1) ↔ ¬ Odd n := by
  simp [Nat.even_add_one]

variable {R : Type*} [AddMonoidWithOne R]

theorem eq_zero_or_one_of_one_add_one (h : (1 : R) + 1 = 0) (n : ℕ):
    (Even n → (n : R) = 0) ∧ (Odd n → (n : R) = 1) := by
  induction n using Nat.twoStepInduction with
  | H1 => simp
  | H2 => simp
  | H3 n IH1 IH2 =>
      rw [one_add_one_eq_two] at h
      simpa only [Nat.succ_eq_add_one, add_assoc, Nat.reduceAdd, Nat.cast_add, Nat.cast_ofNat,
        Nat.even_add_one, Nat.odd_add_one, Decidable.not_not, h, add_zero]

[Ruben Van de Velde]

Or simpa [-Nat.odd_iff_not_even, add_assoc, Nat.even_add_one, Nat.odd_add_one, h]

[Violeta Hernández]

Nice!

[Ruben Van de Velde]

(Those arguments are poorly named)

[Violeta Hernández]

I opened #17483 which (among other things) proves this result