leanprover-community/mathlib3

Pull Requests Commits

feat(category_theory/adjunction): the Special Adjoint Functor Theorem (#15987)

TwoFX committed 3 years ago

c82fab81

feat(data/list/rdrop): drop or take from the right (#15475)

pechersky committed 3 years ago

ed231516

Merge branch 'master' into YK-poincare-metric

urkud committed 3 years ago

f6ce1788

chore(scripts): update nolints.txt (#16305)

leanprover-community-bot committed 3 years ago

3683b34a

feat(ring_theory/unique_factorization_domain): add `associated_iff_normalized_factors_eq_normalized_factors` (#16221)

astrainfinita committed 3 years ago

20f94541

feat(field_theory/normal): Define the normal closure (#16144)

tb65536 committed 3 years ago

17ab30b2

chore(analysis/special_functions): correct typo (#16280)

mcdoll committed 3 years ago

e6c6dfd5

feat(*): replace fact(0 < t) with ne_zero (#16145)

ericrbg committed 3 years ago

879155bf

feat(analysis/normed_space/star/basic): add `cstar_ring` instances for `pi` and `prod` (#16254)

j-loreaux committed 3 years ago

b490ab4a

feat(analysis/seminorm): Add construction of seminorm over normed fields (#15893)

mcdoll committed 3 years ago

d032ed1d

feat(topology): composition of continuous functions is continuous w.r.t. the compact-open topologies (#15721)

faenuccio committed 3 years ago

7e20c8fc

chore(set_theory/cardinal/ordinal): follow your linter (#16265)

adomani committed 3 years ago

1b8a0c29

chore(order/bounded_order): Rename `is_complemented` to `complemented_lattice` (#16263)

YaelDillies committed 3 years ago

daec7d61

feat(order/heyting/regular): Heyting-regular elements (#16033)

YaelDillies committed 3 years ago

24b08ce6

feat(algebra/char_p/basic + data/zmod/basic): the characteristic is the order of one and zmod related lemmas (#16277)

adomani committed 3 years ago

e4b9af26

feat(data/nat/factorization/basic): lemmas about `n.factorization p = 0` (#16185)

stuart-presnell committed 3 years ago

8ad70779

feat(linear_algebra/affine_space/affine_subspace): `map_eq_bot_iff` (#16285)

jsm28 committed 3 years ago

211bf1ab

feat(linear_algebra/affine_space/affine_equiv): lemmas about coercion to `affine_map` (#16284)

jsm28 committed 3 years ago

39d5a98c

feat(data/rat/cast): generalize `ext` lemmas (#16268)

urkud committed 3 years ago

3e2fb4c7

refactor(algebra/order/with_zero): Generalize lemmas (#16240)

YaelDillies committed 3 years ago

31297bda

feat(ring_theory/polynomial/basic): generalize `is_domain` to `no_zero_divisors` (#16226)

eric-wieser committed 3 years ago

301a6253

feat(counterexamples/map_floor): `floor`/`ceil` are not preserved under order ring homs (#16198)

YaelDillies committed 3 years ago

9c0a5431

feat(topology/algebra/polynomial): add coeff_le_of_roots_le (#15275)

xroblot committed 3 years ago

ae93ce85

feat(category_theory/preadditive): projective iff variants of Yoneda preserve epimorphisms (#15123)

TwoFX committed 3 years ago

f0514a8f

feat(algebra/order/positive): new file (#14833)

urkud committed 3 years ago

24a233d4

feat(measure_theory/function/conditional_expectation/basic): add some condexp lemmas (#16273)

kex-y committed 3 years ago

7c4a46f3

feat(data/rat/nnrat): Nonnegative rationals (#16283)

YaelDillies committed 3 years ago

6de241f9

feat(probability/integration): remove integrability assumption in indep_fun.integral_mul (#16167)

sgouezel committed 3 years ago

de62604b

chore(category_theory): fix name of mono_app_of_mono (#16275)

joelriou committed 3 years ago

937c692d

fix(combinatorics/composition): remove non-terminal simp (#16259)

gebner committed 3 years ago

8dd80093

Newer Older