Module

📁 Source: Mathlib/Tactic/Module.lean

Statistics

Metric	Count
Definitions NF, algebraMap, cons, eval, instNeg, instSMulOfMul, «term_::ᵣ_», algebraMapThms, matchScalars, matchScalarsAux, parse, postprocess, qNF, add, matchRings, mkAddProof, mkSubProof, onScalar, sub, toNF, reduceCoefficientwise, tacticMatch_scalars, tacticModule	23
Theorems add_eq_eval, add_eq_eval₁, add_eq_eval₂, add_eq_eval₃, atom_eq_eval, eq_cons_cons, eq_cons_const, eq_const_cons, eq_of_eval_eq_eval, eval_algebraMap, eval_cons, eval_neg, eval_smul, neg_eq_eval, smul_apply, smul_eq_eval, sub_eq_eval, sub_eq_eval₁, sub_eq_eval₂, sub_eq_eval₃, zero_eq_eval, zero_sub_eq_eval	22
Total	45

Mathlib.Tactic.Module

Definitions

Name	Category	Theorems
NF 📖	CompOp	6 math math: NF.eval_neg, NF.smul_apply, NF.zero_sub_eq_eval, NF.neg_eq_eval, NF.eval_smul, NF.smul_eq_eval
algebraMapThms 📖	CompOp	—
matchScalars 📖	CompOp	—
matchScalarsAux 📖	CompOp	—
parse 📖	CompOp	—
postprocess 📖	CompOp	—
qNF 📖	CompOp	—
reduceCoefficientwise 📖	CompOp	—
tacticMatch_scalars 📖	CompOp	—
tacticModule 📖	CompOp	—

Mathlib.Tactic.Module.NF

Definitions

Name	Category	Theorems
algebraMap 📖	CompOp	1 math math: eval_algebraMap
cons 📖	CompOp	10 math math: eq_cons_cons, add_eq_eval₃, eq_cons_const, sub_eq_eval₃, sub_eq_eval₁, sub_eq_eval₂, eq_const_cons, add_eq_eval₂, eval_cons, add_eq_eval₁
eval 📖	CompOp	20 math math: eval_algebraMap, eq_cons_cons, atom_eq_eval, eval_neg, add_eq_eval₃, eq_cons_const, sub_eq_eval₃, sub_eq_eval₁, zero_sub_eq_eval, neg_eq_eval, sub_eq_eval₂, eval_smul, add_eq_eval, zero_eq_eval, eq_const_cons, sub_eq_eval, add_eq_eval₂, smul_eq_eval, eval_cons, add_eq_eval₁
instNeg 📖	CompOp	3 math math: eval_neg, zero_sub_eq_eval, neg_eq_eval
instSMulOfMul 📖	CompOp	3 math math: smul_apply, eval_smul, smul_eq_eval
«term_::ᵣ_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_eq_eval 📖	mathematical	eval AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup eval AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	—
add_eq_eval₁ 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup eval AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass cons	AddSemigroup.toAdd AddMonoid.toAddSemigroup eval AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass cons	—	eval_cons add_assoc
add_eq_eval₂ 📖	mathematical	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup eval AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup eval AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction cons Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	eval_cons add_assoc add_smul add_comm
add_eq_eval₃ 📖	mathematical	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup eval AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction cons	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup eval AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction cons	—	eval_cons add_comm add_assoc
atom_eq_eval 📖	mathematical	—	eval AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoid.toNSMul	—	one_smul add_zero
eq_cons_cons 📖	mathematical	eval AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	eval AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass cons	—	eval_cons
eq_cons_const 📖	mathematical	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring eval AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	eval AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction cons	—	eval_cons zero_smul zero_add
eq_const_cons 📖	mathematical	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring eval AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	eval AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction cons	—	eval_cons zero_smul zero_add
eq_of_eval_eq_eval 📖	—	eval AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	—	—
eval_algebraMap 📖	mathematical	—	eval AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction algebraMap	—	IsScalarTower.algebraMap_smul
eval_cons 📖	mathematical	—	eval AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass cons	—	—
eval_neg 📖	mathematical	—	eval AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction Mathlib.Tactic.Module.NF instNeg NegZeroClass.toNeg Ring.toAddCommGroup	—	List.sum_neg neg_smul
eval_smul 📖	mathematical	eval AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	eval AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Mathlib.Tactic.Module.NF instSMulOfMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	List.smul_sum SemigroupAction.mul_smul
neg_eq_eval 📖	mathematical	eval AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction	NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid eval AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid NegZeroClass.toZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction Mathlib.Tactic.Module.NF instNeg Ring.toAddCommGroup	—	eval_neg
smul_apply 📖	mathematical	—	Mathlib.Tactic.Module.NF instSMulOfMul	—	—
smul_eq_eval 📖	mathematical	eval AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction eval AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Mathlib.Tactic.Module.NF instSMulOfMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	eval_smul
sub_eq_eval 📖	mathematical	eval AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Ring.toSemiring SubNegMonoid.toSub	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup eval AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction	—	—
sub_eq_eval₁ 📖	mathematical	SubNegMonoid.toSub AddGroup.toSubNegMonoid eval AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid cons	SubNegMonoid.toSub AddGroup.toSubNegMonoid eval AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid cons	—	eval_cons sub_eq_add_neg add_assoc
sub_eq_eval₂ 📖	mathematical	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup eval AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup eval AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction cons AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	eval_cons sub_eq_add_neg neg_add add_assoc add_smul neg_smul add_comm
sub_eq_eval₃ 📖	mathematical	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup eval AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction cons	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup eval AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction cons NegZeroClass.toNeg Ring.toAddCommGroup	—	eval_cons sub_eq_add_neg neg_add neg_smul add_comm add_assoc
zero_eq_eval 📖	mathematical	—	AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass eval AddSemigroup.toAdd AddMonoid.toAddSemigroup AddMonoid.toNSMul	—	—
zero_sub_eq_eval 📖	mathematical	—	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid eval AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction Mathlib.Tactic.Module.NF instNeg NegZeroClass.toNeg Ring.toAddCommGroup	—	zero_sub eval_neg

Mathlib.Tactic.Module.qNF

Definitions

Name	Category	Theorems
add 📖	CompOp	—
matchRings 📖	CompOp	—
mkAddProof 📖	CompOp	—
mkSubProof 📖	CompOp	—
onScalar 📖	CompOp	—
sub 📖	CompOp	—
toNF 📖	CompOp	—

---

← Back to Index