leanprover-community/mathlib

Pull Requests Commits

feat(analysis/convex/{basic,function}): add lemmas, golf (#11608)

urkud committed 3 years ago

155c3309

feat(combinatorics/configuration): The order of a projective plane is at least 2 (#11550)

tb65536 committed 3 years ago

a52ce83e

feat (algebraic_geometry): Constructions of fibred products of schemes (#11450)

erdOne committed 3 years ago

9150268c

feat(data/{int,nat}/gcd): add `nat.gcd_greatest` (#11611)

stuart-presnell committed 3 years ago

4a6709bc

feat(topology/uniform_space/uniform_convergence): Product of `tendsto_uniformly` (#11562)

tb65536 committed 3 years ago

bc2f73f7

chore(data/set/lattice): Generalize more `⋃`/`⋂` lemmas to dependent families (#11516)

YaelDillies committed 3 years ago

f99af7da

feat(algebra/lie/cartan_subalgebra): add self-normalizing characterisation for Lie subalgebra (#11598)

ocfnash committed 3 years ago

ee36571e

feat(analysis/normed_space/linear_isometry): `to_linear_equiv_trans` (#11628)

jsm28 committed 3 years ago

dac4f405

feat(group_theory/commuting_probability): Commuting probability inequalities (#11564)

tb65536 committed 3 years ago

ed903019

feat(linear_algebra/orientation): `eq_neg_iff_eq_neg` (#11629)

jsm28 committed 3 years ago

9ef7f6bd

refactor(order/ideal): Generalize definition and lemmas (#11421)

YaelDillies committed 3 years ago

7ddb9a3c

feat(algebra/order/rearrangement) : Rearrangement Inequality (#10861)

MantasBaksys committed 3 years ago

9becbc7c

chore(category_theory/abelian): Moved more stuff into `pseudoelement` locale (#11621)

erdOne committed 3 years ago

8c64be0b

feat(set_theory/surreal/dyadic): define add_monoid_hom structure on dyadic map (#11052)

apurvnakade committed 3 years ago

8f73b079

feat(analysis/asymptotics): add a few lemmas (#11623)

urkud committed 3 years ago

32cd2787

feat(linear_algebra/basis): `reindex_refl` (#11626)

jsm28 committed 3 years ago

095c46c2

feat(data/nat/prime): factors of non-prime powers (#11546)

b-mehta committed 3 years ago

5449ffa4

feat(measure_theory/measure): assorted lemmas (#11612)

urkud committed 3 years ago

59ef8ce5

feat(analysis/calculus/inverse): a map which approximates a linear map on a set admits a nice global extension (#11568)

sgouezel committed 3 years ago

d0f392e1

feat(number_theory/cyclotomic/basic): add missing lemmas (#11451)

riccardobrasca committed 3 years ago

b1ad3012

chore(analysis/normed/group/completion): fix attribution (#11614)

hrmacbeth committed 3 years ago

9a517cf0

chore(data/complex/is_R_or_C): squeeze simps (#11251)

dupuisf committed 3 years ago

2babfeb0

feat(measure_theory/covering): Lebesgue density points (#11554)

sgouezel committed 3 years ago

84dbe7ba

chore(measure_theory/probability_mass_function): Move pmf monad operations into a seperate file (#11579)

dtumad committed 3 years ago

a196f9be

feat(topology/instances/ennreal): continuity of subtraction on ennreal (#11527)

sgouezel committed 3 years ago

31db25b4

split(order/max): Split off `order.basic` (#11603)

YaelDillies committed 3 years ago

159d9aca

feat(topology): add a few lemmas (#11607)

urkud committed 3 years ago

5080d64d

move(order/hom/order): Move from `order.hom.lattice` (#11601)

YaelDillies committed 3 years ago

bd3b892f

doc(group_theory.quotient_group): Fix typos in main statement list (#11581)

nomeata committed 3 years ago

206b56ec

feat(group_theory/abelianization): add mul_equiv.abelianization_congr (#11466)

nomeata committed 3 years ago

155cf1df

Newer Older