Two

📁 Source: Mathlib/Algebra/CharP/Two.lean

Statistics

Metric	Count
Definitions	0
Theorems `sq_inj`, `sq_injective`, `add_cancel_left`, `add_cancel_right`, `add_eq_iff_eq_add`, `add_eq_zero`, `add_mul_self`, `add_self_eq_zero`, `add_sq`, `eq_add_iff_add_eq`, `intCast_cases`, `intCast_eq_ite`, `intCast_eq_mod`, `list_sum_mul_self`, `list_sum_sq`, `multiset_sum_mul_self`, `multiset_sum_sq`, `natCast_cases`, `natCast_eq_ite`, `natCast_eq_mod`, `neg_eq`, `neg_eq'`, `ofNat_eq_mod`, `of_one_ne_zero_of_two_eq_zero`, `range_intCast`, `range_natCast`, `sq_inj`, `sq_injective`, `sub_eq_add`, `sum_mul_self`, `sum_sq`, `two_eq_zero`, `two_nsmul`, `two_zsmul`, `neg_one_eq_one_iff`	35
Total	35

CharTwo

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_cancel_left` 📖	mathematical	—	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`add_assoc` `add_self_eq_zero` `zero_add`
`add_cancel_right` 📖	mathematical	—	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`add_assoc` `add_self_eq_zero` `add_zero`
`add_eq_iff_eq_add` 📖	mathematical	—	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`sub_eq_iff_eq_add` `sub_eq_add`
`add_eq_zero` 📖	mathematical	—	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`sub_eq_add` `sub_eq_iff_eq_add` `zero_add`
`add_mul_self` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Distrib.toAdd`	—	`pow_two` `add_sq`
`add_self_eq_zero` 📖	mathematical	—	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`Nat.instAtLeastTwoHAddOfNat` `two_mul` `two_eq_zero` `MulZeroClass.zero_mul`
`add_sq` 📖	mathematical	—	`Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`Nat.instAtLeastTwoHAddOfNat` `add_pow_two` `ofNat_eq_mod` `Nat.cast_zero` `MulZeroClass.zero_mul` `add_zero`
`eq_add_iff_add_eq` 📖	mathematical	—	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`eq_sub_iff_add_eq` `sub_eq_add`
`intCast_cases` 📖	mathematical	—	`AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`Set.ext_iff` `range_intCast` `Set.mem_range_self`
`intCast_eq_ite` 📖	mathematical	—	`AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `Even` `Int.instDecidablePredEven` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`Int.cast_natCast` `natCast_eq_ite` `Int.cast_neg` `neg_eq`
`intCast_eq_mod` 📖	mathematical	—	`AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne`	—	`intCast_eq_ite`
`list_sum_mul_self` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Distrib.toAdd` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`list_sum_sq`
`list_sum_sq` 📖	mathematical	—	`Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`map_list_sum` `AddMonoidHom.instAddMonoidHomClass`
`multiset_sum_mul_self` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Multiset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Multiset.map`	—	`Multiset.map_congr` `multiset_sum_sq`
`multiset_sum_sq` 📖	mathematical	—	`Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Multiset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Multiset.map`	—	`map_multiset_sum` `AddMonoidHom.instAddMonoidHomClass`
`natCast_cases` 📖	mathematical	—	`AddMonoidWithOne.toNatCast` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddMonoidWithOne.toOne`	—	`Eq.le` `range_natCast` `Set.mem_range_self`
`natCast_eq_ite` 📖	mathematical	—	`AddMonoidWithOne.toNatCast` `Even` `Nat.instDecidablePredEven` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddMonoidWithOne.toOne`	—	`Nat.cast_zero` `Nat.cast_add` `Nat.cast_one` `Nat.instAtLeastTwoHAddOfNat` `one_add_one_eq_two` `two_eq_zero` `zero_add`
`natCast_eq_mod` 📖	mathematical	—	`AddMonoidWithOne.toNatCast`	—	`natCast_eq_ite`
`neg_eq` 📖	mathematical	—	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	—	`neg_eq_iff_add_eq_zero` `add_self_eq_zero`
`neg_eq'` 📖	mathematical	—	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	—	`neg_eq`
`ofNat_eq_mod` 📖	mathematical	—	`AddMonoidWithOne.toNatCast`	—	`natCast_eq_mod`
`of_one_ne_zero_of_two_eq_zero` 📖	mathematical	`instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `Nat.instAtLeastTwoHAddOfNat` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid`	`CharP`	—	`Nat.instAtLeastTwoHAddOfNat` `Nat.even_or_odd` `Even.two_dvd` `natCast_eq_zero_of_even_of_two_eq_zero` `Odd.not_two_dvd_nat` `natCast_eq_one_of_odd_of_two_eq_zero`
`range_intCast` 📖	mathematical	—	`Set.range` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `Set` `Set.instInsert` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Set.instSingletonSet` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`intCast_eq_ite` `Set.range_ite_const`
`range_natCast` 📖	mathematical	—	`Set.range` `AddMonoidWithOne.toNatCast` `Set` `Set.instInsert` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `Set.instSingletonSet` `AddMonoidWithOne.toOne`	—	`natCast_eq_ite` `Set.range_ite_const`
`sq_inj` 📖	mathematical	—	`Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`sq_injective`
`sq_injective` 📖	mathematical	—	`Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`add_eq_zero` `pow_eq_zero_iff` `isReduced_of_noZeroDivisors` `two_ne_zero` `add_sq`
`sub_eq_add` 📖	mathematical	—	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`sub_eq_add_neg` `neg_eq`
`sum_mul_self` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`sum_sq`
`sum_sq` 📖	mathematical	—	`Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`map_sum` `AddMonoidHom.instAddMonoidHomClass`
`two_eq_zero` 📖	mathematical	—	`instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `Nat.instAtLeastTwoHAddOfNat` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid`	—	`Nat.instAtLeastTwoHAddOfNat` `Nat.cast_two` `CharP.cast_eq_zero`
`two_nsmul` 📖	mathematical	—	`AddMonoid.toNSMul` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`two_nsmul` `add_self_eq_zero`
`two_zsmul` 📖	mathematical	—	`SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`two_zsmul` `add_self_eq_zero`

CharTwo.CommRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sq_inj` 📖	mathematical	—	`Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	—
`sq_injective` 📖	mathematical	—	`Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`CharTwo.sq_injective`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`neg_one_eq_one_iff` 📖	mathematical	—	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `ringChar` `Semiring.toNonAssocSemiring` `Ring.toSemiring`	—	`Nat.dvd_prime` `Nat.prime_two` `ringChar.dvd` `Nat.cast_add` `Nat.cast_one` `sub_neg_eq_add` `sub_eq_zero` `CharP.ringChar_ne_one` `CharTwo.neg_eq` `ringChar.of_eq`

---

← Back to Index