Fin

This file provides lemmas about 1-element, 2-element, and 3-element types that are not present in Mathlib.

theorem fin1_eq_fin1 (a b : Fin 1) : a = b

theorem fin2_eq_1_of_ne_0 {a : Fin 2} (ha : a ≠ 0) : a = 1

theorem fin2_eq_0_of_ne_1 {a : Fin 2} (ha : a ≠ 1) : a = 0

theorem fin3_eq_2_of_ne_0_1 {a : Fin 3} (ha0 : a ≠ 0) (ha1 : a ≠ 1) : a = 2

theorem fin3_eq_1_of_ne_0_2 {a : Fin 3} (ha0 : a ≠ 0) (ha2 : a ≠ 2) : a = 1

theorem fin3_eq_0_of_ne_1_2 {a : Fin 3} (ha1 : a ≠ 1) (ha2 : a ≠ 2) : a = 0

theorem Z2_eq_1_of_ne_0 {a : Z2} (ha : a ≠ 0) : a = 1

theorem Z2_eq_0_of_ne_1 {a : Z2} (ha : a ≠ 1) : a = 0

theorem Z3_eq_2_of_ne_0_1 {a : Z3} (ha0 : a ≠ 0) (ha1 : a ≠ 1) : a = 2

theorem Z3_eq_1_of_ne_0_2 {a : Z3} (ha0 : a ≠ 0) (ha2 : a ≠ 2) : a = 1

theorem Z3_eq_0_of_ne_1_2 {a : Z3} (ha1 : a ≠ 1) (ha2 : a ≠ 2) : a = 0

theorem Z2.eq_0_or_1 (a : Z2) : a = 0 ∨ a = 1

theorem Z2_ext {a b : Z2} (hab : ZMod.val a = ZMod.val b) : a = b

theorem Z2_ext_iff (a b : Z2) : a = b ↔ ZMod.val a = ZMod.val b

theorem Z2.valCast_in_signTypeCastRange (x : Z2) : ↑(ZMod.val x) ∈ SignType.cast.range

@[simp]

theorem cast_1_fromZ2_toRat : ZMod.cast 1 = 1

theorem Z2val_toRat_mul_Z2val_toRat (a b : Z2) : ↑(ZMod.val a) * ↑(ZMod.val b) = ↑(ZMod.val (a * b))

theorem Z2_mul_cast_toRat (a b : Z2) : ZMod.cast (a * b) = ZMod.cast a * ZMod.cast b

theorem abs_mul_eq_zmod_cast {a b : Z2} {a' b' : ℚ} (haa : |a'| = ZMod.cast a) (hbb : |b'| = ZMod.cast b) : |a' * b'| = ZMod.cast (a * b)

theorem abs_add_eq_zmod_cast {a b : Z2} {a' b' : ℚ} (haa : |a'| = ZMod.cast a) (hbb : |b'| = ZMod.cast b) (hab : a' + b' ∈ SignType.cast.range) : |a' + b'| = ZMod.cast (a + b)

theorem abs_add_add_eq_zmod_cast {a b c : Z2} {a' b' c' : ℚ} (haa : |a'| = ZMod.cast a) (hbb : |b'| = ZMod.cast b) (hcc : |c'| = ZMod.cast c) (habc : a' + b' + c' ∈ SignType.cast.range) : |a' + b' + c'| = ZMod.cast (a + b + c)

def equivUnitSumUnit : Unit ⊕ Unit ≃ Fin 2

Equations

• One or more equations did not get rendered due to their size.