leanprover-community/mathlib

Pull Requests Commits

feat(data/real/sqrt): add sqrt_div' lemma (#18216)

JovanGerb committed 3 years ago

3b9e2ef2

fix(tactic/ring): perform definitional rather than syntactic matches on `^` (#18156)

eric-wieser committed 3 years ago

c1ada9d1

chore(analysis/normed_space/continuous_linear_map): fix docs typo (#18215)

hrmacbeth committed 3 years ago

e0e2f10d

fix(geometry/euclidean/circumcenter): fix `fintype_finite` lint error (#18213)

jsm28 committed 3 years ago

509de852

refactor(geometry/euclidean/angle/oriented/basic): split out rotations (#18212)

jsm28 committed 3 years ago

fb319896

refactor(geometry/euclidean/angle/unoriented/basic): split out conformal map lemmas (#18210)

jsm28 committed 3 years ago

df78eae5

chore(ring_theory/adjoin_root): fix timeout by writing out `simps` manually (#18209)

Vierkantor committed 3 years ago

97586a95

chore(*): add mathlib4 synchronization comments (#18202)

github-actions[bot] committed 3 years ago

cc70d914

feat (analysis/integrals): integral of x * (1 + x^2)^t (#18201)

loefflerd committed 3 years ago

15a07a99

feat(algebra/triv_sq_zero_ext): lemmas about pow, and ring structure (#18199)

eric-wieser committed 3 years ago

7c3780f6

feat(data/list/of_fn): two lemmas about tuple concatenation (#18192)

eric-wieser committed 3 years ago

fd838fdf

feat(ring_theory/power_basis): matrix of multiplication by generator (#18177)

alreadydone committed 3 years ago

d1d69e99

feat(combinatorics/quiver/single_obj): single object quivers (#17846)

bottine committed 3 years ago

56adee5b

refactor(analysis/normed_space/operator_norm): split (#18205)

hrmacbeth committed 3 years ago

26703ef2

feat(archive/imo/imo2019_q2): IMO 2019 Q2 (#17993)

jsm28 committed 3 years ago

6890b009

feat(ring_theory/*): generalise `minpoly.dvd` to integrally closed rings (#18021)

Paul-Lez committed 3 years ago

cbdf7b56

chore(analysis/normed_space/star/basic): split (#18194)

hrmacbeth committed 3 years ago

3249a849

chore(analysis/normed/field/basic): split (#18195)

hrmacbeth committed 3 years ago

008205aa

feat(data/polynomial): Add Partial Fraction Decomposition (Existence) (#17709)

thefundamentaltheor3m committed 3 years ago

6e70e0d4

chore(*): add mathlib4 synchronization comments (#18196)

github-actions[bot] committed 3 years ago

e04043d6

feat(number_theory/diophantine_approximation): add more results (#18193)

MichaelStollBayreuth committed 3 years ago

9956c380

feat(algebra/order/to_interval_mod): more relations between `to_Ixx_{mod/div}` definitions (#17933)

eric-wieser committed 3 years ago

a993e7ee

feat(group_theory/perm/cycle/basic): Countable sets admit cycles (#17909)

YaelDillies committed 3 years ago

18562995

feat(analysis/seminorm): characterize continuity of seminorms by closed balls (#17249)

ADedecker committed 3 years ago

c46f021f

feat(topology/algebra/equicontinuity): a family of group homomorphisms is equicontinuous iff it is equicontinuous at `1` (#17128)

ADedecker committed 3 years ago

01ad394a

fix(analysis/inner_product_space/basic): restore `bilin_form_of_real_inner` (#18093)

eric-wieser committed 3 years ago

b4f03bc5

chore(analysis/convex/exposed): downgrade imports (#18186)

hrmacbeth committed 3 years ago

48024901

feat(number_theory): prove the existence of infinitely many Fermat pseudoprimes to any base (#17632)

nielsvoss committed 3 years ago

c0439b48

chore(topology/metric_space/isometry): rename isometric to isometry_equiv (#18191)

JovanGerb committed 3 years ago

4b99fe0a

chore(analysis/convex/body): downgrade imports (#18185)

hrmacbeth committed 3 years ago

e6c26fe3

Newer Older