leanprover-community/mathlib

Pull Requests Commits

Merge branch 'alexjbest/fix-zmod-diamond' into alexjbest/hasse

alexjbest committed 3 years ago

b7022a09

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

alexjbest committed 3 years ago

603d910e

alexjbest committed 3 years ago

a236b936

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

feat(measure_theory/integral/circle_integral): add lemma `circle_map_nmem_ball` (#14643)

ocfnash committed 3 years ago

8fb92bf1

feat(number_theory/legendre_symbol/auxiliary, *): add/move lemmas in/to various files, delete `auxiliary.lean` (#14572)

MichaelStollBayreuth committed 3 years ago

d6eb634b

chore(measure_theory): use notation `measurable_set[m]` (#14690)

urkud committed 3 years ago

97c9ef8c

feat(data/{finset,set}/basic): More `insert` and `erase` lemmas (#14675)

YaelDillies committed 3 years ago

8cad81ae

feat(data/polynomial/laurent): Laurent polynomials are a localization of polynomials (#14489)

adomani committed 3 years ago

579d6f9e

feat(number_theory/bernoulli_polynomials): Derivative of Bernoulli polynomial (#14625)

loefflerd committed 3 years ago

4a3b22e5

feat(data/polynomial/eval): add some lemmas for `comp` (#14346)

astrainfinita committed 3 years ago

0926f07a

feat(category_theory/Fintype): equiv_equiv_iso (#13984)

kim-em committed 3 years ago

eb063e78

feat(algebra/char_p): `char_p` of a local ring is zero or prime power (#14461)

Jon Eugster committed 3 years ago

053a03d6

feat(analysis/special_functions/log): add `real.log_sqrt` (#14663)

urkud committed 3 years ago

2e3a0a6e

feat(topology/algebra/module/locally_convex): local convexity is preserved by `Inf` and `induced` (#12118)

ADedecker committed 3 years ago

d1a6dd23

feat(algebra/{group,hom}/units): Units in division monoids (#14212)

YaelDillies committed 3 years ago

13b999c4

feat(group_theory/sylow): Sylow subgroups are Hall subgroups (#14624)

tb65536 committed 3 years ago

050404af

feat(topology/uniform_space/equiv): define uniform isomorphisms (#14537)

ADedecker committed 3 years ago

18936e55

feat(topology/algebra/order): `coe : ℚ → 𝕜` has dense range (#14635)

urkud committed 3 years ago

8c812fd4

feat(data/rat): Add some lemmas to work with num/denom (#14456)

Jon Eugster committed 3 years ago

0f5a1f22

feat(analysis/inner_product_space): Generalize Gram-Schmidt (#14379)

abentkamp committed 3 years ago

95da6493

feat(set_theory/game/ordinal): golf `to_pgame_injective` (#14661)

vihdzp committed 3 years ago

391d1780

refactor(set_theory/game/pgame): rename and add theorems like `-y ≤ -x ↔ x ≤ y` (#14653)

vihdzp committed 3 years ago

68dc07f6

feat(data/fintype/basic): add `card_subtype_mono` (#14645)

linesthatinterlace committed 3 years ago

a9123922

chore(topology/metric_space/basic): add `metric_space.replace_bornology` (#14638)

eric-wieser committed 3 years ago

771f2b7b

refactor(logic/equiv/basic): tweak lemmas on equivalences between `unique` types (#14605)

vihdzp committed 3 years ago

5bccb515

feat(data/polynomial/derivative): reduce assumptions (#14338)

astrainfinita committed 3 years ago

76918216

Older