leanprover-community/mathlib

Pull Requests Commits

feat(ring_theory/ring_hom_properties) : Redefine `stable_under_base_change` in terms of `is_pushout`. (#15805)

erdOne committed 3 years ago

b5aecf07

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

leanprover-community-bot committed 3 years ago

544afa1c

refactor(data/set/n_ary): extract from data/set/basic (#17836)

eric-wieser committed 3 years ago

655994e2

feat(geometry/euclidean/circumcenter): reindexing (#17830)

jsm28 committed 3 years ago

07fee0ca

feat(geometry/euclidean/angle/oriented/affine): angles in pairs of parallel lines (#17829)

jsm28 committed 3 years ago

03c860eb

chore(group_theory/quotient_group): drop unneeded names in `to_additive` (#17821)

urkud committed 3 years ago

0d17cfb6

feat(data/nat/log): review/extend API (#17809)

urkud committed 3 years ago

dc9db541

feat(analysis/convex/between): betweenness in a ring (#17755)

jsm28 committed 3 years ago

41abcdc0

feat(linear_algebra/affine_space/combination): `congr` lemmas (#17659)

jsm28 committed 3 years ago

514ff6b4

feat(linear_algebra/affine_space/finite_dimensional): collinearity and spans of two points (#17635)

jsm28 committed 3 years ago

ab845455

feat(geometry/euclidean/angle/unoriented/affine): collinearity lemma (#17634)

jsm28 committed 3 years ago

2af8cec7

feat(geometry/euclidean/circumcenter): equal circumspheres among cospherical points (#17572)

jsm28 committed 3 years ago

a5abf903

feat(analysis/convex/between): more transitivity variants (#17527)

jsm28 committed 3 years ago

164690af

feat(algebra/cubic_discriminant): add nat degree and monic lemmas (#17780)

Multramate committed 3 years ago

6f11155d

feat(geometry/euclidean/angle/oriented): base angles of isosceles triangles are acute (#17823)

jsm28 committed 3 years ago

10ac9529

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

Newer Older