Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
chore(data/list): move lemmas from data.list.basic that require algeb…
…ra.group_power to a new file (#9728) Hopefully ease the dependencies on anyone importing data.list.basic, if your code broke after this change adding `import data.list.prod_monoid` should fix it. Lemmas moved: - `list.prod_repeat` - `list.sum_repeat` - `list.prod_le_of_forall_le` - `list.sum_le_of_forall_le`
- Loading branch information
Showing
4 changed files
with
44 additions
and
20 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,42 @@ | ||
/- | ||
Copyright (c) 2021 Alex J. Best. All rights reserved. | ||
Released under Apache 2.0 license as described in the file LICENSE. | ||
Authors: Alex J. Best | ||
-/ | ||
import data.list.basic | ||
import algebra.group_power.basic | ||
|
||
/-! | ||
# Products / sums of lists of terms of a monoid | ||
This file provides basic results about `list.prod` (definition in `data.list.defs`) in a monoid. | ||
It is in a separate file so that `data.list.basic` does not depend on `algebra.group_power.basic`. | ||
-/ | ||
|
||
open nat | ||
|
||
namespace list | ||
|
||
universes u v | ||
variables {α : Type u} | ||
|
||
@[simp, priority 500, to_additive] | ||
theorem prod_repeat [monoid α] (a : α) (n : ℕ) : (repeat a n).prod = a ^ n := | ||
begin | ||
induction n with n ih, | ||
{ rw pow_zero, refl }, | ||
{ rw [list.repeat_succ, list.prod_cons, ih, pow_succ] } | ||
end | ||
|
||
@[to_additive] | ||
lemma prod_le_of_forall_le [ordered_comm_monoid α] (l : list α) (n : α) (h : ∀ (x ∈ l), x ≤ n) : | ||
l.prod ≤ n ^ l.length := | ||
begin | ||
induction l with y l IH, | ||
{ simp }, | ||
{ specialize IH (λ x hx, h x (mem_cons_of_mem _ hx)), | ||
have hy : y ≤ n := h y (mem_cons_self _ _), | ||
simpa [pow_succ] using mul_le_mul' hy IH } | ||
end | ||
|
||
end list |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,5 +1,6 @@ | ||
import tactic.lint | ||
import data.list.basic | ||
import algebra.group_power.basic | ||
open tactic | ||
|
||
lemma test_a : true := | ||
|