leanprover-community/mathlib3

Pull Requests Commits

feat(data/fun_like): define `embedding_like` and `equiv_like` (#10759)

Vierkantor committed 3 years ago

494f7199

feat(model_theory/basic): Terms, formulas, and definable sets (#11067)

awainverse committed 3 years ago

6b322417

feat(README.md): add Kyle Miller as new maintainer (#11653)

kmill committed 3 years ago

4883d11c

feat(number_theory/quadratic_reciprocity): generalise legendre_sym to allow integer first argument (#11573)

alexjbest committed 3 years ago

bf71feb0

feat(group_theory/nilpotent): add nilpotency_class inequalities (#11585)

nomeata committed 3 years ago

f7a597ad

feat(README.md): add Frédéric Dupuis as new maintainer (#11651)

dupuisf committed 3 years ago

f2786639

chore(order/filter, *): enhancing `filter_upwards` tactic (#11624)

arthurpaulino committed 3 years ago

b3cd0e6d

refactor(order/{bounded, rel_classes}): Moved `bounded` into the `set` namespace (#11594)

vihdzp committed 3 years ago

8cc2ff4c

chore(topology/metric_space/gromov_hausdorff): Golf some theorems (#11591)

vihdzp committed 3 years ago

b834415b

feat(algebra/big_operators/basic): add lemma `finset.prod_dvd_prod` (#11521)

stuart-presnell committed 3 years ago

88479be0

refactor(tactic/interactive): rename tactic.interactive.triv to tactic.interactive.trivial' (#11643)

kmill committed 3 years ago

4f5d6acf

feat(README.md): add Riccardo Brasca as new maintainer (#11647)

riccardobrasca committed 3 years ago

0d172bac

feat(data/finset/finsupp): Finitely supported product of finsets (#11639)

YaelDillies committed 3 years ago

12fde093

chore(ci): remove working directory on self-hosted (#11645)

gebner committed 3 years ago

32052b86

feat(algebra/pointwise): add partial order to `set_semiring` (#11567)

adomani committed 3 years ago

511aa358

feat(algebra/pointwise): Scalar multiplication lemmas (#11486)

YaelDillies committed 3 years ago

9e799a08

chore(probability_theory/stopping): fix names in documentation (#11644)

kex-y committed 3 years ago

6aea8acc

doc(tactic/interactive): mention triv uses contradiction (#11502)

kbuzzard committed 3 years ago

1bbed968

feat(algebra/lie/nilpotent): generalise lower central series to start with given Lie submodule (#11625)

ocfnash committed 3 years ago

eccd8dd1

feat(analysis/special_functions/pow): add nnreal variant of rpow_pos (#11619)

Ruben-VandeVelde committed 3 years ago

a6318391

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

Newer Older