leanprover-community/mathlib

Pull Requests Commits

Update ordinal_arithmetic.lean

vihdzp committed 3 years ago

66b8229f

Merge branch 'unbounded_refactor' into enum_ord_bdd

vihdzp committed 3 years ago

98a69dc0

chore(algebra/order/ring): add a few aliases (#11911)

urkud committed 3 years ago

b1269b0d

feat(*): localized `R[X]` notation for `polynomial R` (#11895)

pechersky committed 3 years ago

85d9f218

feat(group_theory/submonoid/operations): prod_le_iff and le_prod_iff, also for groups and modules (#11898)

nomeata committed 3 years ago

59325814

refactor(number_theory/bernoulli_polynomials): improve names (#11805)

oxarbitrage committed 3 years ago

2b68801b

feat(analysis/complex): a few lemmas about `dist` and `conj` (#11913)

urkud committed 3 years ago

1077eb3c

feat(linear_algebra/basis): `basis.map_equiv_fun` (#11888)

jsm28 committed 3 years ago

36d3b688

style(analysis/special_functions/trigonometric/angle): make types of `sin` and `cos` explicit (#11902)

jsm28 committed 3 years ago

f94b0b31

feat(topology/sheaf_condition): connect sheaves on sites and on spaces without has_products (#11706)

alreadydone committed 3 years ago

9ceb3c2a

chore(data/finsupp/basic): generalize comap_mul_action (#11900)

eric-wieser committed 3 years ago

436966c1

feat(algebra/big_operators/basic): add multiset.prod_sum (#11885)

Ruben-VandeVelde committed 3 years ago

7b91f008

feat(analysis/inner_product_space/basic): `orthonormal.map_linear_isometry_equiv` (#11893)

jsm28 committed 3 years ago

02c9d69d

feat(analysis/complex/isometry): `rotation_symm` (#11891)

jsm28 committed 3 years ago

c61ea33b

feat(analysis/complex/circle): `exp_map_circle_neg` (#11889)

jsm28 committed 3 years ago

2364a091

feat(analysis/special_functions/trigonometric/angle): `sin`, `cos` (#11887)

jsm28 committed 3 years ago

99215e3d

feat(analysis/special_functions/trigonometric/angle): `induction_on` (#11886)

jsm28 committed 3 years ago

98ef84ef

feat(data/list): add some lemmas. (#11879)

Ruben-VandeVelde committed 3 years ago

26179ccd

feat(category_theory/limits): is_limit.exists_unique (#11875)

TwoFX committed 3 years ago

dcbb59c4

feat(category_theory/limits): (co)equalizers in the opposite category (#11874)

TwoFX committed 3 years ago

556483f4

feat(data/set/opposite): the opposite of a set (#11860)

TwoFX committed 3 years ago

7a2a5468

feat(order/complete_lattice): infi_le_iff (#11810)

PatrickMassot committed 3 years ago

0354e56f

chore(algebra/monoid_algebra): generalize lift_nc (#11881)

eric-wieser committed 3 years ago

a2f3f55e

feat(data/pfun): Composition of partial functions (#11865)

YaelDillies committed 3 years ago

04b9d281

chore(model_theory/*): Split up model_theory/basic (#11846)

awainverse committed 3 years ago

00908913

feat(analysis/normed_space/linear_isometry): `symm_trans` (#11892)

jsm28 committed 3 years ago

3c70566a

refactor(data/quot): Make more `setoid` arguments implicit (#11824)

YaelDillies committed 3 years ago

b1b09eb3

feat(analysis/complex/basic): `conj_lie_symm` (#11890)

jsm28 committed 3 years ago

25297ecf

vihdzp committed 3 years ago

52b39170

vihdzp committed 3 years ago

b890f2ff

Older