Documentation Verification Report

Even

📁 Source: Mathlib/Algebra/Group/Even.lean

Statistics

Metric	Count
Definitions `instDecidablePredEven`, `instDecidablePredIsSquare`, `instDecidablePredAddOppositeEven`, `instDecidablePredMulOppositeIsSquare`	4
Theorems `add`, `add_self`, `exists_add_self`, `exists_two_nsmul`, `isSquare_pow`, `isSquare_zpow`, `map`, `neg`, `nsmul_left`, `nsmul_right`, `sub`, `two_nsmul`, `zero`, `zsmul_left`, `zsmul_right`, `div`, `exists_mul_self`, `exists_sq`, `inv`, `map`, `mul`, `mul_self`, `one`, `pow`, `sq`, `zpow`, `even_iff_exists_add_self`, `even_iff_exists_two_nsmul`, `even_neg`, `even_ofMul_iff`, `even_op_iff`, `even_subset_image_even`, `even_toAdd_iff`, `even_unop_iff`, `isSquare_iff_exists_mul_self`, `isSquare_iff_exists_sq`, `isSquare_inv`, `isSquare_ofAdd_iff`, `isSquare_op_iff`, `isSquare_subset_image_isSquare`, `isSquare_toMul_iff`, `isSquare_unop_iff`	42
Total	46

Additive

Definitions

Name	Category	Theorems
`instDecidablePredEven` 📖	CompOp	—

Even

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	—	`Even` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	—	`add_add_add_comm`
`add_self` 📖	mathematical	—	`Even`	—	—
`exists_add_self` 📖	—	`Even`	—	—	`even_iff_exists_add_self`
`exists_two_nsmul` 📖	mathematical	`Even` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`AddMonoid.toNatSMul`	—	`even_iff_exists_two_nsmul`
`isSquare_pow` 📖	mathematical	`Even`	`IsSquare` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Monoid.toNatPow`	—	`exists_add_self` `pow_add`
`isSquare_zpow` 📖	mathematical	`Even`	`IsSquare` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `DivInvMonoid.toZPow`	—	`exists_add_self` `zpow_add`
`map` 📖	mathematical	`Even` `AddZero.toAdd` `AddZeroClass.toAddZero`	`DFunLike.coe`	—	`map_add` `AddMonoidHomClass.toAddHomClass`
`neg` 📖	mathematical	`Even` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `SubtractionMonoid.toSubNegMonoid`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid`	—	`even_neg`
`nsmul_left` 📖	mathematical	`Even`	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoid.toNatSMul`	—	`exists_add_self` `add_nsmul` `add_self`
`nsmul_right` 📖	mathematical	`Even` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`AddMonoid.toNatSMul`	—	`exists_add_self` `AddCommute.add_nsmul` `AddCommute.refl` `add_self`
`sub` 📖	mathematical	`Even` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `SubtractionMonoid.toSubNegMonoid` `SubtractionCommMonoid.toSubtractionMonoid`	`SubNegMonoid.toSub`	—	`sub_eq_add_neg` `add` `even_neg`
`two_nsmul` 📖	mathematical	—	`Even` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoid.toNatSMul`	—	`two_nsmul`
`zero` 📖	mathematical	—	`Even` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddZero.toZero`	—	`add_zero`
`zsmul_left` 📖	mathematical	`Even`	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SubNegMonoid.toZSMul`	—	`exists_add_self` `add_zsmul` `add_self`
`zsmul_right` 📖	mathematical	`Even` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `SubtractionMonoid.toSubNegMonoid`	`SubNegMonoid.toZSMul`	—	`exists_add_self` `AddCommute.zsmul_add` `AddCommute.refl` `add_self`

IsSquare

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`div` 📖	mathematical	`IsSquare` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `DivisionMonoid.toDivInvMonoid` `DivisionCommMonoid.toDivisionMonoid`	`DivInvMonoid.toDiv`	—	`div_eq_mul_inv` `mul`
`exists_mul_self` 📖	—	`IsSquare`	—	—	`isSquare_iff_exists_mul_self`
`exists_sq` 📖	mathematical	`IsSquare` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`Monoid.toNatPow`	—	`isSquare_iff_exists_sq`
`inv` 📖	mathematical	`IsSquare` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `DivisionMonoid.toDivInvMonoid`	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid`	—	`isSquare_inv`
`map` 📖	mathematical	`IsSquare` `MulOne.toMul` `MulOneClass.toMulOne`	`DFunLike.coe`	—	`map_mul` `MonoidHomClass.toMulHomClass`
`mul` 📖	—	`IsSquare` `CommMagma.toMul` `CommSemigroup.toCommMagma`	—	—	`mul_mul_mul_comm`
`mul_self` 📖	mathematical	—	`IsSquare`	—	—
`one` 📖	mathematical	—	`IsSquare` `MulOne.toMul` `MulOneClass.toMulOne` `MulOne.toOne`	—	`mul_one`
`pow` 📖	mathematical	`IsSquare` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`Monoid.toNatPow`	—	`exists_mul_self` `Commute.mul_pow`
`sq` 📖	mathematical	—	`IsSquare` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Monoid.toNatPow`	—	`pow_two`
`zpow` 📖	mathematical	`IsSquare` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `DivisionMonoid.toDivInvMonoid`	`DivInvMonoid.toZPow`	—	`exists_mul_self` `Commute.mul_zpow`

Multiplicative

Definitions

Name	Category	Theorems
`instDecidablePredIsSquare` 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
`instDecidablePredAddOppositeEven` 📖	CompOp	—
`instDecidablePredMulOppositeIsSquare` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`even_iff_exists_add_self` 📖	mathematical	—	`Even`	—	—
`even_iff_exists_two_nsmul` 📖	mathematical	—	`Even` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoid.toNatSMul`	—	`two_nsmul`
`even_neg` 📖	mathematical	—	`Even` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `SubtractionMonoid.toSubNegMonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid`	—	`neg_neg` `Even.map` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass` `even_op_iff`
`even_ofMul_iff` 📖	mathematical	—	`Even` `Additive` `Additive.add` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Additive.ofMul` `IsSquare`	—	—
`even_op_iff` 📖	mathematical	—	`Even` `AddOpposite` `AddOpposite.instAdd` `AddOpposite.op`	—	—
`even_subset_image_even` 📖	mathematical	`DFunLike.coe`	`Set` `Set.instHasSubset` `setOf` `Even` `AddZero.toAdd` `AddZeroClass.toAddZero` `Set.image`	—	`Even.add_self` `map_add` `AddMonoidHomClass.toAddHomClass`
`even_toAdd_iff` 📖	mathematical	—	`Even` `DFunLike.coe` `Equiv` `Multiplicative` `EquivLike.toFunLike` `Equiv.instEquivLike` `Multiplicative.toAdd` `IsSquare` `Multiplicative.mul`	—	—
`even_unop_iff` 📖	mathematical	—	`Even` `AddOpposite.unop` `AddOpposite` `AddOpposite.instAdd`	—	`even_op_iff`
`isSquare_iff_exists_mul_self` 📖	mathematical	—	`IsSquare`	—	—
`isSquare_iff_exists_sq` 📖	mathematical	—	`IsSquare` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Monoid.toNatPow`	—	`pow_two`
`isSquare_inv` 📖	mathematical	—	`IsSquare` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `DivisionMonoid.toDivInvMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid`	—	`inv_inv` `IsSquare.map` `MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass` `isSquare_op_iff`
`isSquare_ofAdd_iff` 📖	mathematical	—	`IsSquare` `Multiplicative` `Multiplicative.mul` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Multiplicative.ofAdd` `Even`	—	—
`isSquare_op_iff` 📖	mathematical	—	`IsSquare` `MulOpposite` `MulOpposite.instMul` `MulOpposite.op`	—	—
`isSquare_subset_image_isSquare` 📖	mathematical	`DFunLike.coe`	`Set` `Set.instHasSubset` `setOf` `IsSquare` `MulOne.toMul` `MulOneClass.toMulOne` `Set.image`	—	`map_mul` `MonoidHomClass.toMulHomClass`
`isSquare_toMul_iff` 📖	mathematical	—	`IsSquare` `DFunLike.coe` `Equiv` `Additive` `EquivLike.toFunLike` `Equiv.instEquivLike` `Additive.toMul` `Even` `Additive.add`	—	—
`isSquare_unop_iff` 📖	mathematical	—	`IsSquare` `MulOpposite.unop` `MulOpposite` `MulOpposite.instMul`	—	`isSquare_op_iff`

---

← Back to Index