leanprover-community/mathlib3

Pull Requests Commits

Merge branch 'master' into YK-sum-meas-mem-Ioc-le

robertylewis committed 3 years ago

Verified 84618208

feat(linear_algebra/vandermonde): add lemmas about det equals zero (#14695)

bartmichels committed 3 years ago

ed033f39

feat({tactic + test}/congrm, logic/basic): `congrm = congr + pattern-match` (#14153)

adomani committed 3 years ago

41eb9587

feat(topology/homeomorph): add `homeomorph.set.univ` (#14730)

urkud committed 3 years ago

32d8fc4e

feat(analysis/special_functions/exp): add `real.exp_half` (#14729)

urkud committed 3 years ago

1c8f995c

feat(data/complex/basic): ranges of `re`, `im`, `norm_sq`, and `abs` (#14727)

urkud committed 3 years ago

da5a737b

refactor(algebra/order/group): unify instances (#14705)

urkud committed 3 years ago

b11f8e7f

feat(algebra/algebra/basic): define `alg_hom_class` and `non_unital_alg_hom_class` (#14679)

dupuisf committed 3 years ago

2b469927

feat(order/{conditionally_complete_lattice,galois_connection): Supremum of `set.image2` (#14307)

YaelDillies committed 3 years ago

5d18a722

feat(algebra/lie/weights): the zero root space is the Cartan subalgebra for a Noetherian Lie algebra (#14174)

ocfnash committed 3 years ago

300c4395

feat(set_theory/cardinal/cofinality): lemma on subsets of strong limit cardinal (#14442)

vihdzp committed 3 years ago

67dfb57c

fix(data/list/nodup): change `Type` to `Type u` (#14721)

user7230724 committed 3 years ago

7fee0f12

feat(logic/equiv/basic): add `Pi_comm` aka `function.swap` as an `equiv` (#14561)

ADedecker committed 3 years ago

659983c6

refactor(algebra/order/monoid): Split field of `canonically_ordered_...` (#14556)

YaelDillies committed 3 years ago

18bf7af3

refactor(data/option/defs): Swap arguments to `option.elim` (#14681)

YaelDillies committed 3 years ago

2967fae8

feat(set_theory/game/ordinal): golf `to_pgame_birthday` (#14662)

vihdzp committed 3 years ago

425dfe76

doc(ring_theory/algebraic): clarify docstring (#14715)

kbuzzard committed 3 years ago

3afafe6b

feat(category_theory/limits): realise products as pullbacks (#14322)

kim-em committed 3 years ago

b44e742e

feat(algebra/module/pid): Classification of finitely generated torsion modules over a PID (#13524)

pbazin committed 3 years ago

a75460f3

feat(category_theory/monoidal): monoidal functors `Type ⥤ C` acting on powers (#14330)

kim-em committed 3 years ago

3225926b

chore(analysis/locally_convex/weak_dual): golf using `seminorm.comp` (#14699)

eric-wieser committed 3 years ago

6ad27998

feat(data/zmod/basic): fix a diamond in comm_ring and field (#14712)

alexjbest committed 3 years ago

aae786c2

feat(topology/uniform_space/basic): add three easy lemmas about `uniform_space.comap` (#14678)

ADedecker committed 3 years ago

aed7f9af

doc(field_theory/finite/trace): fix module docstring (#14711)

MichaelStollBayreuth committed 3 years ago

b7b371e1

chore(analysis/complex/upper_half_plane): move to a subdirectory (#14704)

urkud committed 3 years ago

46ac3cb3

chore(algebra/big_operators/associated,ring_theory/unique_factorization_domain): golf (#14671)

Ruben-VandeVelde committed 3 years ago

04019de3

refactor(order/conditionally_complete_lattice): use `order_bot` (#14568)

urkud committed 3 years ago

b1000376

chore(algebra/ring_quot): provide an explicit npow field (#14349)

eric-wieser committed 3 years ago

4b676457

feat(set_theory/surreal/dyadic): tweak API + golf (#14649)

vihdzp committed 3 years ago

716824d3

feat(tactic/lift): generalize pi.can_lift to Sort (#14700)

kmill committed 3 years ago

dc9eab66

Older