leanprover-community/mathlib

Pull Requests Commits

Merge branch 'SP_disjoint_prod_add' into SP_multiplicative_fn_factorization

stuart-presnell committed 4 years ago

739cbb33

Add lemma `multiplicative_factorization` (proof incomplete)

stuart-presnell committed 4 years ago

be018dc9

Replace with shorter proof

stuart-presnell committed 4 years ago

0f516fb2

stuart-presnell committed 4 years ago

337d6f2f

Rewrite `...aux` lemma as `have` statement; delete `aux` lemma

stuart-presnell committed 4 years ago

30bf2e91

Move body of `..aux` into main proof

stuart-presnell committed 4 years ago

5fb1678b

Change brackets per reviewer suggestion

stuart-presnell committed 4 years ago

66c5616e

Rename to `prod_add_index_of_disjoint`; reverse order of equality

stuart-presnell committed 4 years ago

b00a5ba7

Move up out of `map_range` section; wrap in section for typeclassing

stuart-presnell committed 4 years ago

0d92ddd6

Docstring for `disjoint_prod_add`

stuart-presnell committed 4 years ago

30b6e868

Fixed proof of `disjoint_prod_add_aux`

stuart-presnell committed 4 years ago

24a1af3d

Failing to recover a proof

stuart-presnell committed 4 years ago

2ccf8beb

Template for `disjoint_prod_add` with `sorry`

stuart-presnell committed 4 years ago

de8990d5

Change `factorization_mul_of_pos` to `factorization_mul`

stuart-presnell committed 4 years ago

509fd17a

Add docstring to `factorization_mul_of_pos`

stuart-presnell committed 4 years ago

e86edfeb

Add `factorization_mul_of_pos`

stuart-presnell committed 4 years ago

e450f190

Add `count_factors_mul_of_pos` to `data/nat/prime`

stuart-presnell committed 4 years ago

48795ef1

Change `nil` to `zero`

stuart-presnell committed 4 years ago

8de6906f

Replace `factorization_eq_iff` with `factorization_inj`

stuart-presnell committed 4 years ago

558e4e42

Delete prime_factorization.lean

stuart-presnell committed 4 years ago

99a7641d

Create factorization.lean

stuart-presnell committed 4 years ago

f93979e6

Change `'prime_factorization` to `factorization` throughout

stuart-presnell committed 4 years ago

46480851

Comment formatting; rename some lemmas

stuart-presnell committed 4 years ago

869c719b

Rename `prime_factorization_count` to `prime_factorization_eq_count`

stuart-presnell committed 4 years ago

a9a085fa

feat(measure_theory/integral/set_to_l1): various properties of the set_to_fun construction (#10713)

RemyDegenne committed 4 years ago

e3eb0eb0

feat(algebraic_geometry): LocallyRingedSpace has coproducts. (#10665)

erdOne committed 4 years ago

1367c19b

feat(algebra/group): make `map_[z]pow` generic in `monoid_hom_class` (#10749)

Vierkantor committed 4 years ago

9078914e

chore(data/equiv/ring): inv_fun_eq_symm (#10779)

pechersky committed 4 years ago

f46a7a0f

feat(combinatorics/simple_graph): simp lemmas about spanning coe (#10778)

b-mehta committed 4 years ago

6d15ea43

feat(group_theory/order_of_element): additivize (#10766)

ericrbg committed 4 years ago

05d87671

Older