Prod

Statistics

Metric	Count
Definitions	0
Theorems `isLinearMap_add`, `isLinearMap_sub`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`isLinearMap_add` 📖	mathematical	—	`IsLinearMap` `Prod.instAddCommMonoid` `Prod.instModule` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`Mathlib.Tactic.Abel.subst_into_add` `Mathlib.Tactic.Abel.term_atom` `Mathlib.Tactic.Abel.term_add_const` `zero_add` `Mathlib.Tactic.Abel.const_add_term` `smul_add`
`isLinearMap_sub` 📖	mathematical	—	`IsLinearMap` `Prod.instAddCommMonoid` `AddCommGroup.toAddCommMonoid` `Prod.instModule` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`sub_eq_add_neg` `neg_add_rev` `add_comm` `add_assoc` `add_left_comm` `smul_sub`

---