Documentation Verification Report

AdditiveCombination

📁 Source: PrimeNumberTheoremAnd/Tactic/AdditiveCombination.lean

Statistics

MetricCount
DefinitionsAdditiveCombination, elabAdditiveCombination, expandAdditiveCombo
3
Theoremsc_smul_pf, pf_smul_c, smul_pf
3
Total6

Mathlib.Tactic.LinearCombination'

Definitions

NameCategoryTheorems
AdditiveCombination 📖CompOp
elabAdditiveCombination 📖CompOp
expandAdditiveCombo 📖CompOp

Theorems

NameKindAssumesProvesValidatesDepends On
c_smul_pf 📖
pf_smul_c 📖
smul_pf 📖

---

← Back to Index