Commits leanprover-community/mathlib

feat(data/polynomial): irreducibility criteria for (quadratic) monic polynomials (#17664)

alreadydone committed 3 years ago

fa256f00

feat(dynamics/ergodic/add_circle): ergodicity of zsmul on the additive circle (#17544)

ocfnash committed 3 years ago

7679be23

feat(topology/algebra/module/strong_topology): strong topology on continuous linear maps is locally convex and T2 (#16794)

ADedecker committed 3 years ago

62f682c0

feat(topology/uniform_space/equicontinuity): definition and basic properties of [uniform] equicontinuity (#16467)

ADedecker committed 3 years ago

41e1ab75

feat(algebra/hom/equiv/basic): Add `to_additive` to `Pi_congr_right` lemmas (#17827)

winstonyin committed 3 years ago

e753057a

chore(logic/basic): golf a proof (#17807)

urkud committed 3 years ago

10ee5ede

chore(*): add mathlib4 synchronization comments (#17806)

leanprover-community-bot committed 3 years ago

8770c841

chore(number_theory/padics): fix lemma names and golf (#17798)

eric-wieser committed 3 years ago

b9b2114f

chore(data/polynomial/derivative): change n to C n (#17795)

Multramate committed 3 years ago

d7744511

feat(category_theory/idempotents): universal property of karoubi (#17603)

joelriou committed 3 years ago

631175a8

feat(linear_algebra/affine_space/independent): `affine.simplex.reindex` (#17566)

jsm28 committed 3 years ago

38375881

feat(linear_algebra/affine_space/affine_subspace): `parallel` and affine spans (#17526)

jsm28 committed 3 years ago

8348e173

feat(set_theory/cardinal): add lemmas about `n : ℕ` and `ℵ₀` (#17490)

urkud committed 3 years ago

49605783

move(algebra/order/monoid/*): relocate `zero_le_one_class` again (#17820)

astrainfinita committed 3 years ago

428acaae

chore(data/set/constructions): Make `has_finite_inter` Prop-valued (#17824)

YaelDillies committed 3 years ago

a95b16cb

feat(analysis/special_functions/trigonometric/angle): twice angles adding to `π` (#17822)

jsm28 committed 3 years ago

77314cca

feat(combinatorics/quiver/*) `cast` arrows and paths along equalities (#17617)

bottine committed 3 years ago

6ed79339

feat(order/upper_lower): More `prod` lemmas (#17747)

YaelDillies committed 3 years ago

97b62c86

chore(algebra/ring/defs): refactor `is_domain` (#17721)

riccardobrasca committed 3 years ago

b1d911ac

chore(algebra/big_operators/basic): golf results about bUnion (#17501)

eric-wieser committed 3 years ago

62ec8656

feat(measure_theory/integrals): integration by parts for algebra-valued functions (#17778)

loefflerd committed 3 years ago

347d2ed1

feat(geometry/euclidean/angle/oriented/affine): more collinearity / affine independence lemmas (#17815)

jsm28 committed 3 years ago

6959abed

feat(algebraic_topology/dold_kan): N₂ reflects isomorphisms (#17577)

joelriou committed 3 years ago

88bca0ce

refactor(algebraic_geometry/EllipticCurve): generalise elliptic curves into weierstrass curves (#17220)

Multramate committed 3 years ago

c0dd3fc8

feat(algebraic_topology/dold_kan): the inverse functor of the Dold-Kan equivalence (#17607)

joelriou committed 3 years ago

dd1f8496

feat(analysis/special_functions/trigonometric/angle): `to_real` lemmas (#17395)

jsm28 committed 3 years ago

f1a2caaf

chore(data/{finset,set}/basic): Align lemmas (#17805)

YaelDillies committed 3 years ago

a50170a8

feat(*/sub*/pointwise): lemmas about pointwise scalar actions (#17814)

eric-wieser committed 3 years ago

c982179e

chore(analysis/inner_product_space/rayleigh): squeeze a simp (#17811)

adomani committed 3 years ago

ce613251

feat(algebra/order/zero_le_one): generalize lemmas (#17465)

astrainfinita committed 3 years ago

9b2660e1