leanprover-community/mathlib3

Pull Requests Commits

use alias for fields of is_expansion_on

fpvandoorn committed 3 years ago

dfe9e051

chore(*): bump to lean 3.47.0 (#16252)

digama0 committed 3 years ago

3d7987cd

feat(linear_algebra/finite_dimensional): `dim_add_le_dim_add_dim` (#16301)

jsm28 committed 3 years ago

fbfe26dc

feat(algebraic_topology): the category simplicial_object.split (#16274)

joelriou committed 3 years ago

86e93623

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

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

Older