leanprover-community/mathlib

Pull Requests Commits

j-loreaux committed 3 years ago

Verified c59a5989

show `star_alg_hom`s and friends are order preserving for `star_ordered_ring`s

j-loreaux committed 3 years ago

Verified 491c492a

j-loreaux committed 3 years ago

Verified c4fbbb55

feat(algebra/star/basic): basic lemmas for `star_ordered_ring`

j-loreaux committed 3 years ago

Verified 7f921b27

feat(algebra/algebra/spectrum): add a few basic lemmas for convenience (#17156)

j-loreaux committed 3 years ago

11dcb6b5

feat(data/set/basic): add `sum.range_eq` (#17159)

urkud committed 3 years ago

db0b5669

feat(topology/instances/add_circle): the additive circle is a divisible group (#17138)

ocfnash committed 3 years ago

45f23a64

feat(tactic/push_neg): #push_neg user command (#16775)

hrmacbeth committed 3 years ago

822af854

chore(bar): drop empty file (#17208)

ocfnash committed 3 years ago

ca53494a

src(dynamics/ergodic/ergodic): define ergodic maps / measures (#17046)

ocfnash committed 3 years ago

9743845b

chore: freeze data.option.defs (#17195)

javra committed 3 years ago

3248c520

feat(data/set/basic): `pair_eq_pair_iff` (#17187)

kmill committed 3 years ago

324f6d55

chore(order/bounded_order): remove unnecessary imports (#17180)

kim-em committed 3 years ago

c571859d

feat(geometry/euclidean/angle/unoriented/right_angle): trigonometric lemmas (#17173)

jsm28 committed 3 years ago

6bc0c198

feat(algebra/gcd_monoid): normalization and gcd are subsingletons given unique units (#17149)

Vierkantor committed 3 years ago

b30d648a

feat(measure_theory/measure/haar): add lemma `measure_theory.measure.measure_preserving_zpow` (#17137)

ocfnash committed 3 years ago

ec22570c

feat(measure_theory/integral/periodic): the volume measure on the additive circle is doubling (#17031)

ocfnash committed 3 years ago

9fb40d5a

chore(topology/sheaf_condition): is_sheaf_iff_pairwise_intersections without products (#17181)

alreadydone committed 3 years ago

20e597fb

chore(category_theory/groupoid/*) More subgroupoid lemmas (#17147)

bottine committed 3 years ago

14c11403

refactor(topology/bases): removing/adding the empty set from/to a basis (#17133)

alreadydone committed 3 years ago

dc2a9659

feat(analysis/calculus/uniform_limits_deriv): pointwise convergence out of derivative convergence on a preconnected set (#17123)

sgouezel committed 3 years ago

1a249186

feat(order/filter/ultrafilter): an ultrafilter is an atom in the lattice of filters (#17116)

urkud committed 3 years ago

c680de9e

feat(analysis/convex/side): connectedness of sides (#16938)

jsm28 committed 3 years ago

4b6fbb3e

feat(is_cyclotomic_extension/basic): add is_cyclotomic_extension.equiv (#16757)

riccardobrasca committed 3 years ago

1acf2b9a

feat(topology/sheaves/*): Notation for restriction of sections. (#16088)

erdOne committed 3 years ago

06c75afe

feat(data/nat/interval): Cauchy induction (#15880)

Shimonschlessinger committed 3 years ago

9340cc93

feat(analysis/normed_space/hahn_banach/separation): generalize to (locally convex) topological vector spaces (#16796)

ADedecker committed 3 years ago

bcf8d82b

feat({data, analysis}/complex/basic): lemmas related to `complex.partial_order` (#17170)

j-loreaux committed 3 years ago

05f9a362

feat(data/set/intervals/basic): Injectivity of half-infinite intervals (#17157)

mans0954 committed 3 years ago

438381a5

chore(data/set/pointwise): split file, reducing dependencies (#16950)

kim-em committed 3 years ago

aa329229

Older