leanprover-community/mathlib3

Pull Requests Commits

Split out `monoid Ioc`

stuart-presnell committed 4 years ago

4a7699d6

stuart-presnell committed 4 years ago

24f43c35

Draft: `comm_monoid (Ioc 0 1)`

stuart-presnell committed 4 years ago

c8403130

Templates for other instances

stuart-presnell committed 4 years ago

8938abb1

Separate `semigroup Ico` from `comm_semigroup Ico`

stuart-presnell committed 4 years ago

e69e1d00

Draft: ocs α => cs (Ico 0 1)

stuart-presnell committed 4 years ago

8bdcf59c

Delete separate `semigroup` instance

stuart-presnell committed 4 years ago

bf87a494

Condense `npow_succ'`

stuart-presnell committed 4 years ago

031a1915

Extract `semigroup`; expand `simp`s

stuart-presnell committed 4 years ago

4bc44f91

stuart-presnell committed 4 years ago

fed9769a

Draft: extend to `comm_monoid_with_zero`

stuart-presnell committed 4 years ago

b794e9f0

`[ordered_semiring α] => monoid (Icc (0:α) 1)`

stuart-presnell committed 4 years ago

008941b8

Paste in Yaël's comment

stuart-presnell committed 4 years ago

7fb9e299

Add `has_pow [0,1] ℕ`

stuart-presnell committed 4 years ago

97fa93aa

Add `prob_pow_Icc`

stuart-presnell committed 4 years ago

e01b6d53

Create instances.lean

stuart-presnell committed 4 years ago

84879e37

feat(order/cover): Covering elements are unique (#14156)

YaelDillies committed 4 years ago

4cf20164

feat (group_theory/perm/cycles): Add missing `is_cycle` lemma (#13219)

MantasBaksys committed 4 years ago

00e80a63

chore(logic/equiv): golf equiv.subtype_equiv (#14125)

ericrbg committed 4 years ago

c1091050

feat(linear_algebra/matrix): invariant basis number for matrices (#13845)

kim-em committed 4 years ago

843240b0

move(data/prod/*): A `prod` folder (#13771)

YaelDillies committed 4 years ago

f9f64f37

chore(order/lattice): reflow, golf (#14151)

urkud committed 4 years ago

a74298d8

chore(order/conditionally_complete_lattice): General cleanup (#13319)

vihdzp committed 4 years ago

5c954e12

refactor(set_theory/game/*): Fix bad notation `<` on (pre-)games (#13963)

vihdzp committed 4 years ago

b8d8a5e4

feat(linear_algebra/projection) : projections are conjugate to prod_map id 0 (#13802)

antoinelab01 committed 4 years ago

1f00800d

feat(analysis/special_functions/exp_deriv): generalize some lemmas about `complex.exp`, remove `*.cexp_real` (#13579)

astrainfinita committed 4 years ago

e7386121

feat(category_theory): missing comp_ite lemma (#14143)

kim-em committed 4 years ago

570db888

feat(algebra/big_operators): prod_ite_irrel (#14142)

kim-em committed 4 years ago

ad5edeb5

chore(set_theory/ordinal/{basic, arithmetic}): Remove redundant `function` namespace (#14133)

vihdzp committed 4 years ago

05997bda

doc(data/real/sqrt): Fix typo in described theorem (#14126)

timotree3 committed 4 years ago

9d022d77

Newer Older