leanprover-community/mathlib3

Pull Requests Commits

chore(order/filter/basic): protect 3 lemmas (#18331)

urkud committed 3 years ago

24e75f1e

chore(order/upper_lower): split file (#18330)

urkud committed 3 years ago

2769416a

feat(data/quot): make `trunc` a `quotient` (#18320)

astrainfinita committed 3 years ago

6ed6abbd

feat(algebra/order/floor): `0 < fract a ↔ a ≠ ⌊a⌋` (#18317)

MichaelStollBayreuth committed 3 years ago

afdb4342

feat(ring_theory): definition and properties of relative ideal norm (#18299)

Vierkantor committed 3 years ago

8233a1cb

chore(order/filter, topology/algebra): golf (#18097)

urkud committed 3 years ago

78f647f8

feat(algebra/periodic): generalize some lemmas (#18334)

urkud committed 3 years ago

b64b1f88

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

github-actions[bot] committed 3 years ago

13a5329a

feat(data/{bool,set}): add 3 lemmas (#18332)

urkud committed 3 years ago

ed60ee25

refactor(topology/{order,*}): review API (#18312)

urkud committed 3 years ago

bcfa7268

chore(number_theory/cyclotomic/gal): tidy docs (#18326)

ericrbg committed 3 years ago

861a2692

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

github-actions[bot] committed 3 years ago

68d1483e

chore(ring_theory/fractional_ideal): remove instance name (#18305)

Multramate committed 3 years ago

48cb182b

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

github-actions[bot] committed 3 years ago

fac36901

chore(*): rename locale `topological_space` to `topology` (#18293)

urkud committed 3 years ago

f2ce6086

fix(data/set_like): unbundled subclasses of `out_param` classes should not repeat the parents' `out_param` (#18291)

Vierkantor committed 3 years ago

feb99064

feat(ring_theory): lemmas on algebra norm (#18298)

Vierkantor committed 3 years ago

5fe29816

chore(topology/metric_space/anti_lipschitz): fix typo (#18263)

JovanGerb committed 3 years ago

97f079b7

feat(ring_theory/ideal/local_ring): API for local rings. (#17185)

erdOne committed 3 years ago

b86c528d

feat(order/height): The height of a poset (#15026)

erdOne committed 3 years ago

bf277444

feat(algebra/module/graded_module): define graded module (#14582)

jjaassoonn committed 3 years ago

59cdeb0d

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

github-actions[bot] committed 3 years ago

a11f9106

feat(set_theory/zfc/basic): more trivial results (#18294)

vihdzp committed 3 years ago

fedcb65c

feat(analysis/special_functions/trigonometric): Euler's infinite product for sine (part a) (#18282)

loefflerd committed 3 years ago

a1ddb551

chore(ring_theory): protect `algebra.is_integral` (#18178)

alreadydone committed 3 years ago

825edd3c

feat(data/list/lemmas): Range of `foldr` (#13328)

vihdzp committed 3 years ago

975c8c32

feat(number_theory/kummer_dedekind): the return of the Dedekind-Kummer theorem. (#16870)

Paul-Lez committed 3 years ago

f7fc89d5

feat(set_theory/zfc/basic): `pSet.equiv.comm` (#18297)

vihdzp committed 3 years ago

cd45082b

feat(data/real/pi): refactor Wallis formula for pi (#18280)

loefflerd committed 3 years ago

9b94375a

feat(special_functions/integrals): integral of `cos(a * x)` for `a` complex (#18279)

loefflerd committed 3 years ago

2ef3da38

Newer Older