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	6 math math: eq_cons_cons, eq_cons_const, sub_eq_eval₂, eq_const_cons, add_eq_eval₂, eval_cons
eval 📖	CompOp	6 math math: eval_algebraMap, atom_eq_eval, eval_neg, zero_sub_eq_eval, zero_eq_eval, eval_cons
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 📖	—	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	—	—	—
add_eq_eval₁ 📖	—	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	cons Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	eval_cons add_assoc add_smul add_comm
add_eq_eval₃ 📖	—	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.toNatSMul	—	one_smul add_zero
eq_cons_cons 📖	mathematical	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	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	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	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 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	Mathlib.Tactic.Module.NF instSMulOfMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	eval_smul
sub_eq_eval 📖	—	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	—	—	—
sub_eq_eval₁ 📖	—	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	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	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.toNatSMul	—	—
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