leanprover-community/mathlib

Pull Requests Commits

The class number is one iff the ring of integers is a PID

Vierkantor committed 4 years ago

e378bc77

Vierkantor committed 4 years ago

1d20b440

Some example code for ℚ(√-5)

Vierkantor committed 4 years ago

b88524f2

Merge remote-tracking branch 'mathlib/dedekind-domain-dev' into dedekind-domain-dev

Vierkantor committed 4 years ago

ffd0f6ea

Update `is_noetherian_ring` and `ideal.is_maximal`

Vierkantor committed 4 years ago

e7f5b277

Make `is_separable` an instance parameter

Vierkantor committed 4 years ago

5c98f4eb

Update `is_noetherian_ring` definition

Vierkantor committed 4 years ago

f4b22c93

Merge remote-tracking branch 'mathlib/master' into dedekind-domain-WIP

Vierkantor committed 4 years ago

7c5ed969

Update `mul_mem_{left,right}`

Vierkantor committed 4 years ago

05f17abb

`subtype_congr` -> `subtype_equiv` renaming

Vierkantor committed 4 years ago

46344d78

These lemmas were already merged into mathlib

Vierkantor committed 4 years ago

0c1410a8

Update `trace.lean`

Vierkantor committed 4 years ago

c90fda63

Update some more of `minpoly`

Vierkantor committed 4 years ago

2f39a5a6

Generalize some `ordered_comm_monoid` results

Vierkantor committed 4 years ago

0449e68c

Update `minpoly` in `power_basis`

Vierkantor committed 4 years ago

a9a6dd58

Vierkantor committed 4 years ago

1923629e

Explicitize a few parameters

Vierkantor committed 4 years ago

cabc1992

Move power basis of `intermediate_field.adjoin` to `field_theory/adjoin.lean`

Vierkantor committed 4 years ago

4a03991e

Generalize `nat_degree_multiset_prod`

Vierkantor committed 4 years ago

fe3bf4b9

feat(topology/continuous_map): missing coe_mk lemma (#6087)

kim-em committed 4 years ago

90702a04

feat(finset/lattice): max'_insert (#6089)

kim-em committed 4 years ago

a6fc6bdc

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

leanprover-community-bot committed 4 years ago

6b83e728

chore(analysis/calculus/local_extr): review (#6085)

urkud committed 4 years ago

5bf92e1d

feat(topology/separation): an injective map on a compact space is an embedding (#6057)

sgouezel committed 4 years ago

45f95448

feat(algebra/lie/basic): define the center of a Lie algebra and prove some related results (#6013)

ocfnash committed 4 years ago

9411b00e

feat(measure_theory/lebesgue_measure): integral as volume between graphs (#5932)

asouther4 committed 4 years ago

d989ff47

chore(measure_theory): use `∞` notation for `(⊤ : ℝ≥0∞)` (#6080)

urkud committed 4 years ago

f3b0295a

feat(analysis): prove that a polynomial function is equivalent to its leading term along at_top, and consequences (#5354)

ADedecker committed 4 years ago

5d4d8158

refactor(measure_theory/ae_eq_fun): move emetric to `ae_eq_fun_metric` (#6081)

sgouezel committed 4 years ago

99fe12af

chore(measure_theory/measure_space): move definition of `measure.ae` up (#6051)

urkud committed 4 years ago

5a25827e

Older