Documentation

Seymour.Basic.SignTypeCast

SignType and its images #

This file provides lemmas about SignType.cast.range (that is, {0, ±1} in various types) that are not present in Mathlib.

source
theorem zero_iff_ratCast_zero_of_in_signTypeCastRange {a : ℚ} (ha : a ∈ SignType.cast.range) :
a = 0 ↔ ↑a = 0
source
theorem ratCast_eq_intCast_ratFloor_of_in_signTypeCastRange {a : ℚ} (ha : a ∈ SignType.cast.range) :
↑a = ↑a.floor
source
@[simp]
theorem zero_in_signTypeCastRange {R : Type} [NonAssocRing R] :
0 ∈ SignType.cast.range
source
@[simp]
theorem one_in_signTypeCastRange {R : Type} [NonAssocRing R] :
1 ∈ SignType.cast.range
source
@[simp]
theorem neg_one_in_signTypeCastRange {R : Type} [NonAssocRing R] :
-1 ∈ SignType.cast.range
source
@[simp]
theorem SignType.cast_ne_one_add_one {R : Type} [Ring R] [CharZero R] (s : SignType) :
↑s ≠ 1 + 1
source
@[simp]
theorem SignType.cast_ne_neg_one_sub_one {R : Type} [Ring R] [CharZero R] (s : SignType) :
↑s ≠ -1 - 1
source
@[simp]
theorem SignType.cast_ne_neg_one_add_neg_one {R : Type} [Ring R] [CharZero R] (s : SignType) :
↑s ≠ -1 + -1
source
theorem in_signTypeCastRange_mul_in_signTypeCastRange {R : Type} [NonAssocRing R] {a b : R} (ha : a ∈ SignType.cast.range) (hb : b ∈ SignType.cast.range) :
a * b ∈ SignType.cast.range
source
theorem neg_one_mul_in_signTypeCastRange {R : Type} [NonAssocRing R] {a : R} (ha : a ∈ SignType.cast.range) :
-1 * a ∈ SignType.cast.range
source
theorem neg_in_signTypeCastRange {R : Type} [NonAssocRing R] {a : R} (ha : a ∈ SignType.cast.range) :
-a ∈ SignType.cast.range
source
theorem in_signTypeCastRange_of_neg_one_mul {R : Type} [NonAssocRing R] {a : R} (ha : -1 * a ∈ SignType.cast.range) :
a ∈ SignType.cast.range
source
theorem in_signTypeCastRange_of_neg {R : Type} [NonAssocRing R] {a : R} (ha : -a ∈ SignType.cast.range) :
a ∈ SignType.cast.range
source
theorem in_signTypeCastRange_iff_abs {R : Type} [LinearOrderedCommRing R] (a : R) :
a ∈ SignType.cast.range ↔ |a| ∈ SignType.cast.range
source
theorem inv_eq_self_of_in_signTypeCastRange {R : Type} [DivisionRing R] {a : R} (ha : a ∈ SignType.cast.range) :
1 / a = a
source
theorem neg_one_pow_in_signTypeCastRange {R : Type} [Ring R] (k : ℕ) :
(-1) ^ k ∈ SignType.cast.range
source
theorem neg_one_pow_mul_in_signTypeCastRange {R : Type} [Ring R] {a : R} (ha : a ∈ SignType.cast.range) (k : ℕ) :
(-1) ^ k * a ∈ SignType.cast.range