Lemmas

📁 Source: Mathlib/Tactic/FieldSimp/Lemmas.lean

Statistics

Metric	Count
Definitions `NF`, `cons`, `eval`, `instInv`, `instPowInt`, `instPowNat`, `«term_::ᵣ_»`, `div`, `expr`, `inv`, `mkEqMul`, `mul`, `mulRight`, `neg`, `pow`, `zpow`, `zpow'`	17
Theorems `atom_eq_eval`, `cons_eq_div_of_eq_div`, `cons_eq_div_of_eq_div'`, `cons_ne_zero`, `cons_pos`, `cons_zero_eq_div_of_eq_div`, `div_eq_eval`, `div_eq_eval₁`, `div_eq_eval₂`, `div_eq_eval₃`, `eval_cons`, `eval_cons_eq_eval_of_eq_of_eq`, `eval_cons_mul_eval`, `eval_cons_mul_eval_cons_neg`, `eval_cons_of_pow_eq_zero`, `eval_inv`, `eval_mul_eval_cons`, `eval_mul_eval_cons_zero`, `eval_pow`, `eval_zpow'`, `inv_eq_eval`, `mul_eq_eval`, `mul_eq_eval₁`, `mul_eq_eval₂`, `mul_eq_eval₃`, `one_div_eq_eval`, `one_eq_eval`, `pow_apply`, `pow_eq_eval`, `zpow_apply`, `zpow_eq_eval`, `eq_div_of_eq_one_of_subst`, `eq_div_of_eq_one_of_subst'`, `eq_div_of_subst`, `eq_eq_cancel_eq`, `eq_mul_of_eq_eq_eq_mul`, `le_eq_cancel_le`, `list_prod_zpow'`, `lt_eq_cancel_lt`, `mul_zpow'`, `one_zpow'`, `subst_add`, `subst_sub`, `zero_zpow'`, `zpow'_add`, `zpow'_eq_zero_iff`, `zpow'_mul`, `zpow'_neg`, `zpow'_ofNat`, `zpow'_of_ne_zero_left`, `zpow'_of_ne_zero_right`, `zpow'_one`, `zpow'_zero_eq_div`, `zpow'_zero_of_ne_zero`	54
Total	71

Mathlib.Tactic.FieldSimp

Definitions

Name	Category	Theorems
`NF` 📖	CompOp	9 math math: `NF.eval_inv`, `NF.one_div_eq_eval`, `NF.zpow_apply`, `NF.pow_eq_eval`, `NF.zpow_eq_eval`, `NF.eval_zpow'`, `NF.eval_pow`, `NF.pow_apply`, `NF.inv_eq_eval`
`zpow'` 📖	CompOp	17 math math: `zpow'_one`, `one_zpow'`, `NF.eval_zpow'`, `NF.eval_pow`, `zpow'_of_ne_zero_right`, `list_prod_zpow'`, `zpow'_of_ne_zero_left`, `zpow'_eq_zero_iff`, `zpow'_mul`, `zpow'_neg`, `zpow'_zero_eq_div`, `zpow'_ofNat`, `zpow'_add`, `zpow'_zero_of_ne_zero`, `NF.eval_cons`, `zero_zpow'`, `mul_zpow'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_div_of_eq_one_of_subst` 📖	—	`DivInvMonoid.toDiv` `DivInvOneMonoid.toDivInvMonoid` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass`	—	—	`div_one`
`eq_div_of_eq_one_of_subst'` 📖	mathematical	`DivInvMonoid.toDiv` `DivInvOneMonoid.toDivInvMonoid` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass`	`InvOneClass.toInv`	—	`one_div`
`eq_div_of_subst` 📖	—	—	—	—	—
`eq_eq_cancel_eq` 📖	—	`MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass`	—	—	`mul_right_inj'`
`eq_mul_of_eq_eq_eq_mul` 📖	—	—	—	—	—
`le_eq_cancel_le` 📖	mathematical	`MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero`	`Preorder.toLE`	—	`mul_le_mul_iff_right₀`
`list_prod_zpow'` 📖	mathematical	—	`zpow'` `CommGroupWithZero.toGroupWithZero` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid`	—	`one_zpow'` `mul_zpow'` `map_list_prod` `MonoidHom.instMonoidHomClass`
`lt_eq_cancel_lt` 📖	—	`MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero`	—	—	`mul_lt_mul_iff_of_pos_left`
`mul_zpow'` 📖	mathematical	—	`zpow'` `CommGroupWithZero.toGroupWithZero` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	—	`MulZeroClass.zero_mul` `zero_zpow'` `MulZeroClass.mul_zero` `GroupWithZero.noZeroDivisors` `mul_zpow`
`one_zpow'` 📖	mathematical	—	`zpow'` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid`	—	`NeZero.one` `GroupWithZero.toNontrivial` `one_zpow`
`subst_add` 📖	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toAdd`	—	—	`mul_add` `Distrib.leftDistribClass`
`subst_sub` 📖	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	—	`mul_sub`
`zero_zpow'` 📖	mathematical	—	`zpow'` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	—	`zero_zpow`
`zpow'_add` 📖	mathematical	—	`zpow'` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	—	`mul_ite` `MulZeroClass.mul_zero` `ite_mul` `MulZeroClass.zero_mul` `add_zero` `zero_zpow` `zpow_add₀`
`zpow'_eq_zero_iff` 📖	mathematical	—	`zpow'` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	—	`eq_or_ne` `zpow_zero` `NeZero.one` `GroupWithZero.toNontrivial` `zpow_eq_zero_iff`
`zpow'_mul` 📖	mathematical	—	`zpow'`	—	`zero_zpow'` `MulZeroClass.mul_zero` `zpow_zero` `MulZeroClass.zero_mul` `NeZero.one` `GroupWithZero.toNontrivial` `one_zpow` `IsDomain.to_noZeroDivisors` `Int.instIsDomain` `zpow_mul`
`zpow'_neg` 📖	mathematical	—	`zpow'` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid`	—	`zpow_neg` `inv_zero` `zpow_zero` `inv_one` `NeZero.one` `GroupWithZero.toNontrivial`
`zpow'_ofNat` 📖	mathematical	—	`zpow'` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero`	—	`zpow'_of_ne_zero_right` `Nat.cast_zero` `Int.instCharZero` `zpow_natCast`
`zpow'_of_ne_zero_left` 📖	mathematical	—	`zpow'` `DivInvMonoid.toZPow` `GroupWithZero.toDivInvMonoid`	—	—
`zpow'_of_ne_zero_right` 📖	mathematical	—	`zpow'` `DivInvMonoid.toZPow` `GroupWithZero.toDivInvMonoid`	—	—
`zpow'_one` 📖	mathematical	—	`zpow'`	—	`zpow_one`
`zpow'_zero_eq_div` 📖	mathematical	—	`zpow'` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid`	—	`zpow_zero` `div_zero` `div_self`
`zpow'_zero_of_ne_zero` 📖	mathematical	—	`zpow'` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid`	—	`zpow_zero`

Mathlib.Tactic.FieldSimp.NF

Definitions

Name	Category	Theorems
`cons` 📖	CompOp	11 math math: `eval_cons_mul_eval`, `cons_pos`, `div_eq_eval₂`, `eval_mul_eval_cons`, `cons_eq_div_of_eq_div'`, `cons_eq_div_of_eq_div`, `eval_cons_mul_eval_cons_neg`, `mul_eq_eval₂`, `eval_cons`, `cons_zero_eq_div_of_eq_div`, `eval_cons_of_pow_eq_zero`
`eval` 📖	CompOp	8 math math: `eval_inv`, `one_div_eq_eval`, `eval_zpow'`, `eval_pow`, `atom_eq_eval`, `one_eq_eval`, `eval_cons`, `eval_cons_of_pow_eq_zero`
`instInv` 📖	CompOp	3 math math: `eval_inv`, `one_div_eq_eval`, `inv_eq_eval`
`instPowInt` 📖	CompOp	3 math math: `zpow_apply`, `zpow_eq_eval`, `eval_zpow'`
`instPowNat` 📖	CompOp	3 math math: `pow_eq_eval`, `eval_pow`, `pow_apply`
`«term_::ᵣ_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`atom_eq_eval` 📖	mathematical	—	`eval`	—	`Mathlib.Tactic.FieldSimp.zpow'_one` `mul_one`
`cons_eq_div_of_eq_div` 📖	mathematical	`eval` `CommGroupWithZero.toGroupWithZero` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid`	`cons`	—	`eval_cons` `div_eq_mul_inv` `Semigroup.to_isAssociative` `CommMagma.to_isCommutative`
`cons_eq_div_of_eq_div'` 📖	mathematical	`eval` `CommGroupWithZero.toGroupWithZero` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid`	`cons`	—	`eval_cons` `div_eq_mul_inv` `Mathlib.Tactic.FieldSimp.zpow'_neg` `mul_inv` `Semigroup.to_isAssociative` `CommMagma.to_isCommutative`
`cons_ne_zero` 📖	—	—	—	—	`mul_ne_zero` `GroupWithZero.noZeroDivisors`
`cons_pos` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `eval`	`cons`	—	`mul_pos` `Mathlib.Tactic.FieldSimp.zpow'_of_ne_zero_left` `LT.lt.ne'` `zpow_pos`
`cons_zero_eq_div_of_eq_div` 📖	mathematical	`eval` `CommGroupWithZero.toGroupWithZero` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid`	`cons`	—	`add_neg_cancel` `eval_cons` `div_eq_mul_inv` `Mathlib.Tactic.FieldSimp.zpow'_add` `mul_inv` `Semigroup.to_isAssociative` `CommMagma.to_isCommutative`
`div_eq_eval` 📖	—	`eval` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid`	—	—	—
`div_eq_eval₁` 📖	—	`DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid` `CommGroupWithZero.toGroupWithZero` `eval` `cons`	—	—	`eval_cons` `div_eq_mul_inv` `Semigroup.to_isAssociative` `CommMagma.to_isCommutative`
`div_eq_eval₂` 📖	mathematical	`DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid` `CommGroupWithZero.toGroupWithZero` `eval`	`cons`	—	`eval_cons` `div_eq_mul_inv` `mul_inv` `sub_eq_add_neg` `Mathlib.Tactic.FieldSimp.zpow'_add` `Semigroup.to_isAssociative` `CommMagma.to_isCommutative`
`div_eq_eval₃` 📖	—	`DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid` `CommGroupWithZero.toGroupWithZero` `eval` `cons`	—	—	`eval_cons` `div_eq_mul_inv` `mul_inv` `mul_assoc` `Mathlib.Tactic.FieldSimp.zpow'_neg`
`eval_cons` 📖	mathematical	—	`eval` `CommGroupWithZero.toGroupWithZero` `cons` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `Mathlib.Tactic.FieldSimp.zpow'`	—	`mul_comm`
`eval_cons_eq_eval_of_eq_of_eq` 📖	—	`eval` `CommGroupWithZero.toGroupWithZero` `cons`	—	—	`eval_cons`
`eval_cons_mul_eval` 📖	mathematical	`MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `eval`	`cons`	—	`eval_cons` `Semigroup.to_isAssociative` `CommMagma.to_isCommutative`
`eval_cons_mul_eval_cons_neg` 📖	mathematical	`MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `eval`	`cons`	—	`mul_eq_eval₂` `add_neg_cancel` `eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_zero_of_ne_zero` `mul_one`
`eval_cons_of_pow_eq_zero` 📖	mathematical	—	`eval` `CommGroupWithZero.toGroupWithZero` `cons`	—	`eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_zero_of_ne_zero` `mul_one`
`eval_inv` 📖	mathematical	—	`eval` `CommGroupWithZero.toGroupWithZero` `Mathlib.Tactic.FieldSimp.NF` `instInv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid`	—	`List.prod_inv` `Mathlib.Tactic.FieldSimp.zpow'_neg`
`eval_mul_eval_cons` 📖	mathematical	`MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `eval`	`cons`	—	`eval_cons` `mul_assoc`
`eval_mul_eval_cons_zero` 📖	—	`MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `eval` `cons`	—	—	`eval_mul_eval_cons`
`eval_pow` 📖	mathematical	—	`eval` `CommGroupWithZero.toGroupWithZero` `Mathlib.Tactic.FieldSimp.NF` `instPowNat` `Mathlib.Tactic.FieldSimp.zpow'`	—	`eval_zpow'`
`eval_zpow'` 📖	mathematical	—	`eval` `CommGroupWithZero.toGroupWithZero` `Mathlib.Tactic.FieldSimp.NF` `instPowInt` `Mathlib.Tactic.FieldSimp.zpow'`	—	`Mathlib.Tactic.FieldSimp.list_prod_zpow'` `mul_comm`
`inv_eq_eval` 📖	mathematical	`eval` `CommGroupWithZero.toGroupWithZero`	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Mathlib.Tactic.FieldSimp.NF` `instInv`	—	`eval_inv`
`mul_eq_eval` 📖	—	`eval` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	—	—	—
`mul_eq_eval₁` 📖	—	`MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `eval` `cons`	—	—	`eval_cons` `Semigroup.to_isAssociative` `CommMagma.to_isCommutative`
`mul_eq_eval₂` 📖	mathematical	`MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `eval`	`cons`	—	`eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_add` `Semigroup.to_isAssociative` `CommMagma.to_isCommutative`
`mul_eq_eval₃` 📖	—	`MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `eval` `cons`	—	—	`eval_cons` `Semigroup.to_isAssociative` `CommMagma.to_isCommutative`
`one_div_eq_eval` 📖	mathematical	—	`DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid` `CommGroupWithZero.toGroupWithZero` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `eval` `Mathlib.Tactic.FieldSimp.NF` `instInv`	—	`one_div` `eval_inv`
`one_eq_eval` 📖	mathematical	—	`InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `eval`	—	—
`pow_apply` 📖	mathematical	—	`Mathlib.Tactic.FieldSimp.NF` `instPowNat`	—	—
`pow_eq_eval` 📖	mathematical	`eval` `CommGroupWithZero.toGroupWithZero`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `Mathlib.Tactic.FieldSimp.NF` `instPowNat`	—	`eval_pow` `Mathlib.Tactic.FieldSimp.zpow'_ofNat`
`zpow_apply` 📖	mathematical	—	`Mathlib.Tactic.FieldSimp.NF` `instPowInt`	—	—
`zpow_eq_eval` 📖	mathematical	`eval` `CommGroupWithZero.toGroupWithZero`	`DivInvMonoid.toZPow` `GroupWithZero.toDivInvMonoid` `Mathlib.Tactic.FieldSimp.NF` `instPowInt`	—	`Mathlib.Tactic.FieldSimp.zpow'_of_ne_zero_right` `eval_zpow'`

Mathlib.Tactic.FieldSimp.Sign

Definitions

Name	Category	Theorems
`div` 📖	CompOp	—
`expr` 📖	CompOp	—
`inv` 📖	CompOp	—
`mkEqMul` 📖	CompOp	—
`mul` 📖	CompOp	—
`mulRight` 📖	CompOp	—
`neg` 📖	CompOp	—
`pow` 📖	CompOp	—
`zpow` 📖	CompOp	—

---

← Back to Index