Abel

Statistics

Metric	Count
Definitions `AbelMode`, `Config`, `mode`, `toConfig`, `Context`, `app`, `inst`, `isGroup`, `mkApp`, `univ`, `α`, `α0`, `NormalExpr`, `e`, `isAtom`, `term'`, `zero'`, `abel1`, `abel1!`, `abelConv`, `abelNF`, `abelNFConv`, `addG`, `cleanup`, `convAbel!`, `convAbel_nf!_`, `elabAbelNFConfig`, `elabAbelNFConv`, `eval`, `evalAdd`, `evalAtom`, `evalExpr`, `evalNeg`, `evalSMul`, `evalSMul'`, `iapp`, `instCoeNormalExprExpr`, `instInhabitedNormalExpr`, `default`, `intToExpr`, `isAtom`, `mkContext`, `mkTerm`, `smul`, `smulg`, `tacticAbel!`, `tacticAbel_nf!__`, `term`, `termg`	49
Theorems `const_add_term`, `const_add_termg`, `subst_into_add`, `subst_into_addg`, `subst_into_negg`, `subst_into_smul`, `subst_into_smul_upcast`, `subst_into_smulg`, `term_add_const`, `term_add_constg`, `term_add_term`, `term_add_termg`, `term_atom`, `term_atom_pf`, `term_atom_pfg`, `term_atomg`, `term_eq`, `term_neg`, `term_smul`, `term_smulg`, `termg_eq`, `unfold_smul`, `unfold_smulg`, `unfold_sub`, `unfold_zsmul`, `zero_smul`, `zero_smulg`, `zero_term`, `zero_termg`	29
Total	78

Mathlib.Tactic.Abel

Definitions

Name	Category	Theorems
`AbelMode` 📖	CompData	—
`Context` 📖	CompData	—
`NormalExpr` 📖	CompData	—
`abel1` 📖	CompOp	—
`abel1!` 📖	CompOp	—
`abelConv` 📖	CompOp	—
`abelNF` 📖	CompOp	—
`abelNFConv` 📖	CompOp	—
`addG` 📖	CompOp	—
`cleanup` 📖	CompOp	—
`convAbel!` 📖	CompOp	—
`convAbel_nf!_` 📖	CompOp	—
`elabAbelNFConfig` 📖	CompOp	—
`elabAbelNFConv` 📖	CompOp	—
`eval` 📖	CompOp	—
`evalAdd` 📖	CompOp	—
`evalAtom` 📖	CompOp	—
`evalExpr` 📖	CompOp	—
`evalNeg` 📖	CompOp	—
`evalSMul` 📖	CompOp	—
`evalSMul'` 📖	CompOp	—
`iapp` 📖	CompOp	—
`instCoeNormalExprExpr` 📖	CompOp	—
`instInhabitedNormalExpr` 📖	CompOp	—
`intToExpr` 📖	CompOp	—
`isAtom` 📖	CompOp	—
`mkContext` 📖	CompOp	—
`mkTerm` 📖	CompOp	—
`smul` 📖	CompOp	2 math math: `subst_into_smul_upcast`, `zero_smul`
`smulg` 📖	CompOp	1 math math: `zero_smulg`
`tacticAbel!` 📖	CompOp	—
`tacticAbel_nf!__` 📖	CompOp	—
`term` 📖	CompOp	8 math math: `term_add_term`, `term_add_const`, `zero_term`, `const_add_term`, `term_atom`, `term_atom_pf`, `term_smul`, `term_eq`
`termg` 📖	CompOp	9 math math: `const_add_termg`, `term_atomg`, `zero_termg`, `term_neg`, `term_smulg`, `term_add_constg`, `termg_eq`, `term_add_termg`, `term_atom_pfg`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`const_add_term` 📖	mathematical	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	`term`	—	`add_comm` `add_assoc`
`const_add_termg` 📖	mathematical	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	`termg`	—	`add_comm` `add_assoc`
`subst_into_add` 📖	—	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	—	—
`subst_into_addg` 📖	—	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	—	—
`subst_into_negg` 📖	—	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—	—
`subst_into_smul` 📖	—	`smul`	—	—	—
`subst_into_smul_upcast` 📖	mathematical	`smulg`	`smul` `AddCommGroup.toAddCommMonoid`	—	`natCast_zsmul`
`subst_into_smulg` 📖	—	`smulg`	—	—	—
`term_add_const` 📖	mathematical	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	`term`	—	`add_assoc`
`term_add_constg` 📖	mathematical	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	`termg`	—	`add_assoc`
`term_add_term` 📖	mathematical	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	`term`	—	`add_assoc` `add_left_comm` `add_nsmul`
`term_add_termg` 📖	mathematical	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	`termg`	—	`add_zsmul` `add_add_add_comm`
`term_atom` 📖	mathematical	—	`term` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`one_nsmul` `add_zero`
`term_atom_pf` 📖	mathematical	—	`term` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`one_nsmul` `add_zero`
`term_atom_pfg` 📖	mathematical	—	`termg` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`one_zsmul` `add_zero`
`term_atomg` 📖	mathematical	—	`termg` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`one_zsmul` `add_zero`
`term_eq` 📖	mathematical	—	`term` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid`	—	—
`term_neg` 📖	mathematical	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`termg`	—	`neg_add_rev` `neg_zsmul` `add_comm`
`term_smul` 📖	mathematical	`smul`	`term`	—	`nsmul_add` `mul_nsmul'`
`term_smulg` 📖	mathematical	`smulg`	`termg`	—	`zsmul_add` `mul_zsmul`
`termg_eq` 📖	mathematical	—	`termg` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	—
`unfold_smul` 📖	mathematical	`smul`	`AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid`	—	—
`unfold_smulg` 📖	mathematical	`smulg`	`SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	—
`unfold_sub` 📖	mathematical	`AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `SubtractionMonoid.toSubNegMonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid`	`SubNegMonoid.toSub`	—	`sub_eq_add_neg`
`unfold_zsmul` 📖	mathematical	`smulg`	`SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	—
`zero_smul` 📖	mathematical	—	`smul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`nsmul_zero`
`zero_smulg` 📖	mathematical	—	`smulg` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`zsmul_zero`
`zero_term` 📖	mathematical	—	`term`	—	`zero_nsmul` `zero_add`
`zero_termg` 📖	mathematical	—	`termg`	—	`zero_zsmul` `zero_add`

Mathlib.Tactic.Abel.AbelNF

Definitions

Name	Category	Theorems
`Config` 📖	CompData	—

Mathlib.Tactic.Abel.AbelNF.Config

Definitions

Name	Category	Theorems
`mode` 📖	CompOp	—
`toConfig` 📖	CompOp	—

Mathlib.Tactic.Abel.Context

Definitions

Name	Category	Theorems
`app` 📖	CompOp	—
`inst` 📖	CompOp	—
`isGroup` 📖	CompOp	—
`mkApp` 📖	CompOp	—
`univ` 📖	CompOp	—
`α` 📖	CompOp	—
`α0` 📖	CompOp	—

Mathlib.Tactic.Abel.NormalExpr

Definitions

Name	Category	Theorems
`e` 📖	CompOp	—
`isAtom` 📖	CompOp	—
`term'` 📖	CompOp	—
`zero'` 📖	CompOp	—

Mathlib.Tactic.Abel.instInhabitedNormalExpr

Definitions

Name	Category	Theorems
`default` 📖	CompOp	—

---

← Back to Index