leanprover-community/mathlib

Pull Requests Commits

Merge branch 'henselian-rings' of https://github.com/leanprover-community/mathlib into henselian-rings

Ashwin Iyengar committed 5 years ago

f8cdb074

Ashwin Iyengar committed 5 years ago

638a7981

initial commit, defn of henselian

Ashwin Iyengar committed 5 years ago

e4459839

Merge branch 'henselian-rings' of https://github.com/leanprover-community/mathlib into henselian-rings

Ashwin Iyengar committed 5 years ago

00471cec

Ashwin Iyengar committed 5 years ago

f9edb463

initial commit, defn of henselian

Ashwin Iyengar committed 5 years ago

74c674d3

Merge branch 'henselian-rings' of https://github.com/leanprover-community/mathlib into henselian-rings

Ashwin Iyengar committed 5 years ago

951b877b

initial commit, defn of henselian

Ashwin Iyengar committed 5 years ago

0f7bcf6b

feat(data/polynomial): is_unit_C (#2812)

ChrisHughes24 committed 5 years ago

52b839f3

feat(linear_algebra/projection): add `equiv_prod_of_surjective_of_is_compl` (#2787)

urkud committed 5 years ago

3e0668e0

feat(logic/function): define `semiconj` and `commute` (#2788)

urkud committed 5 years ago

60f0b012

feat(algebra/group_power): int.nat_abs_pow_two (#2811)

ChrisHughes24 committed 5 years ago

96f318c5

feat(data/zmod): lemmas about coercions to zmod (#2802)

kim-em committed 5 years ago

9da47ada

feat(data/nat/prime): pow_not_prime (#2810)

ChrisHughes24 committed 5 years ago

dd062f02

chore(topology/algebra/module): prove `fst.prod snd = id` (#2806)

urkud committed 5 years ago

a2d50075

chore(set_theory/ordinal): use a `protected lemma` to drop a `nolint` (#2805)

urkud committed 5 years ago

ccf646d3

fix(tactic/norm_num): workaround int.sub unfolding bug (#2804)

digama0 committed 5 years ago

a3b3aa62

feat(algebra/add_torsor): torsors of additive group actions (#2720)

jsm28 committed 5 years ago

6552f21e

feat(data/int/basic): eq_zero_of_dvd_of_nonneg_of_lt (#2803)

kim-em committed 5 years ago

518d0fd9

feat(char_p): generalize zmod.neg_one_ne_one (#2796)

kim-em committed 5 years ago

8d352b20

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

leanprover-community-bot committed 5 years ago

61b57cd7

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

leanprover-community-bot committed 5 years ago

1445e088

feat(category_theory): Product comparison (#2753)

b-mehta committed 5 years ago

8590081f

feat(category_theory): adjunction convenience defs (#2754)

b-mehta committed 5 years ago

292fc042

feat(linear_algebra/basic): range of `linear_map.prod` (#2785)

urkud committed 5 years ago

2ef444af

chore(order/basic): change "minimum" in descriptions to "minimal" (#2789)

kckennylau committed 5 years ago

5449203f

doc(archive/100-theorems-list): Update README.md (#2750)

jalex-stark committed 5 years ago

79e296bd

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

leanprover-community-bot committed 5 years ago

2a3f59a1

feat(ring_theory/ideal_operations): lemmas about ideals and galois connections (#2767)

ChrisHughes24 committed 5 years ago

2b79f1da

chore(order/basic): add `monotone.order_dual`, `strict_mono.order_dual` (#2778)

urkud committed 5 years ago

ceb13bad

Older