LinearCombination'

Statistics

Metric	Count
Definitions `Expanded`, `elabLinearCombination'`, `expStx`, `expandLinearCombo`, `linearCombination'`, `normStx`, `tacticLinear_combination2____`	7
Theorems `add_pf`, `c_add_pf`, `c_div_pf`, `c_mul_pf`, `c_sub_pf`, `div_pf`, `eq_of_add`, `eq_of_add_pow`, `eq_trans₃`, `inv_pf`, `mul_pf`, `neg_pf`, `pf_add_c`, `pf_div_c`, `pf_mul_c`, `pf_sub_c`, `sub_pf`	17
Total	24

Name	Kind	Assumes	Proves	Validates	Depends On
`add_pf` 📖	—	—	—	—	—
`c_add_pf` 📖	—	—	—	—	—
`c_div_pf` 📖	—	—	—	—	—
`c_mul_pf` 📖	—	—	—	—	—
`c_sub_pf` 📖	—	—	—	—	—
`div_pf` 📖	—	—	—	—	—
`eq_of_add` 📖	—	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	—	`sub_eq_zero`
`eq_of_add_pow` 📖	—	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	—	`sub_eq_zero` `eq_zero_of_pow_eq_zero` `isReduced_of_noZeroDivisors`
`eq_trans₃` 📖	—	—	—	—	—
`inv_pf` 📖	—	—	—	—	—
`mul_pf` 📖	—	—	—	—	—
`neg_pf` 📖	—	—	—	—	—
`pf_add_c` 📖	—	—	—	—	—
`pf_div_c` 📖	—	—	—	—	—
`pf_mul_c` 📖	—	—	—	—	—
`pf_sub_c` 📖	—	—	—	—	—
`sub_pf` 📖	—	—	—	—	—

---