leanprover-community/mathlib3

Pull Requests Commits

JakobScholbach committed 4 years ago

17706c67

JakobScholbach committed 4 years ago

d7193d1e

simplify using .elim

JakobScholbach committed 4 years ago

a24cbd11

fix merge conflicts in src/algebra/char_p/exp_char.lean

JakobScholbach committed 4 years ago

44625737

JakobScholbach committed 4 years ago

8b325247

JakobScholbach committed 4 years ago

f9ebde6f

feat(category_theory/subobject): well-powered categories (#6802)

kim-em committed 4 years ago

6e5c07bf

feat(data/finset): inj on of image card eq (#6785)

b-mehta committed 4 years ago

19483ae3

feat(data/equiv/fintype): computable bijections and perms from/to fintype (#6959)

pechersky committed 4 years ago

73377021

feat(group_theory/order_of_element): generalised to add_order_of (#6770)

Julian-Kuelshammer committed 4 years ago

d8de5672

JakobScholbach committed 4 years ago

79613f51

simplifications

JakobScholbach committed 4 years ago

6a042a4b

admin(README.md): add @adamtopaz to the maintainers list (#6987)

kim-em committed 4 years ago

1e27fba8

admin(README.md): add @b-mehta to the maintainers list (#6986)

kim-em committed 4 years ago

c35e9f63

feat(algebra/char_p/exp_char): basics about the exponential characteristic (#6671)

JakobScholbach committed 4 years ago

cea8c65a

feat(algebra/module/hom): Add missing smul instances on add_monoid_hom (#6891)

eric-wieser committed 4 years ago

396602bf

admin(README.md): add @TwoFX to the maintainers list (#6985)

kim-em committed 4 years ago

a690ce77

fix(algebraic_topology): fix a typo (#6991)

TwoFX committed 4 years ago

132ae2b2

feat(combinatorics/quiver): weakly connected components (#6847)

dwarn committed 4 years ago

a9b6230a

feat(data/equiv/basic): `perm_congr` group lemmas (#6982)

pechersky committed 4 years ago

21cc8066

feat(data/equiv/basic): `equiv.swap_eq_refl_iff` (#6983)

pechersky committed 4 years ago

3365c443

refactor(topology/metric_space/pi_Lp): generalize to pseudo_metric (#6978)

riccardobrasca committed 4 years ago

64abe48e

chore(data/equiv/add_equiv): missing simp lemmas (#6975)

eric-wieser committed 4 years ago

b7fbc17a

feat(data/set/basic): default_coe_singleton (#6971)

pechersky committed 4 years ago

e540c2fe

chore(data/fintype/basic): add card_le_of_surjective and card_quotient_le (#6964)

AdrianDoM committed 4 years ago

ec9476fd

refactor(topology/bases): use `structure` for `is_topological_basis (#6947)

urkud committed 4 years ago

71c3e714

refactor(algebra/*): add new `mul_one_class` and `add_zero_class` for non-associative monoids (#6865)

eric-wieser committed 4 years ago

5f1b4500

feat(data/list/zip): `nth_zip_with` univ polymorphic, `zip_with_eq_nil_iff` (#6974)

pechersky committed 4 years ago

cc991528

feat(tactic/elementwise): autogenerate lemmas in concrete categories (#6941)

kim-em committed 4 years ago

23dbb4cf

feat(category_theory/lifting_properties): create a new file about lifting properties (#6852)

JakobScholbach committed 4 years ago

f29b0b49

Older