leanprover-community/mathlib

Pull Requests Commits

finish profinite group iso, add some LTE

101damnations committed 3 years ago

ab9dc26e

show profinite groups are limits of finite groups

101damnations committed 3 years ago

0a5393c6

one sorry left wahoo

101damnations committed 3 years ago

a2ee9d9e

having a nice profinite time

101damnations committed 3 years ago

9b9a6f2c

golfed hilbert 90 i believe. i need oleans

101damnations committed 3 years ago

fc32d017

101damnations committed 3 years ago

3e729929

101damnations committed 3 years ago

0ed15ca8

starting fixing stuff

101damnations committed 3 years ago

9700ed94

Merge branch 'monoid-algebra-basis2' of https://github.com/leanprover-community/mathlib into group-cohomology

101damnations committed 3 years ago

6d63130d

apply suggestions

101damnations committed 3 years ago

61018217

Merge branch 'master' of https://github.com/leanprover-community/mathlib into monoid-algebra-basis2

101damnations committed 3 years ago

620c18b0

101damnations committed 3 years ago

1df021be

feat(ring_theory/bezout): Bezout domains are integrally closed (#15424)

erdOne committed 3 years ago

7b43177d

refactor(order/compactly_generated): Generalize `submodule.exists_finset_of_mem_supr` to compact elements of complete lattices (#15419)

tb65536 committed 3 years ago

ee72cf62

feat(ring_theory/localization/basic): section of localisation of non-zero is non-zero (#15404)

Multramate committed 3 years ago

0e30f2da

feat(algebraic_geometry/EllipticCurve): simplify definition of discriminant (#15365)

digama0 committed 3 years ago

582e6672

refactor(data/finset/lattice): sup' and inf' without option (#15195)

pechersky committed 3 years ago

bcc2c4e4

feat(tactic/congrm): add "function underscores" to `congrm` (#14532)

adomani committed 3 years ago

9c7a7cca

feat(algebra/module/localized_module): construction of module localisation (#14470)

jjaassoonn committed 3 years ago

fba86201

feat(ring_theory/adjoin_root): add lemmas for GCD domains (#14981)

riccardobrasca committed 3 years ago

903e8941

remove >100 char line

101damnations committed 3 years ago

2f8e4c7c

remove rogue file

101damnations committed 3 years ago

6424485f

101damnations committed 3 years ago

af786ead

feat(data/real/{e,}nnreal): images and preimages of `ord_connected` sets (#15483)

urkud committed 3 years ago

b60a2703

feat(data/list/basic): last_reverse (#15482)

pechersky committed 3 years ago

ed513f85

doc(set_theory/cardinal/basic): tweak documentation (#15480)

vihdzp committed 3 years ago

a641e1b6

feat(algebra/order/monoid): add `one_lt_mul_iff`/`add_pos_iff` (#15458)

urkud committed 3 years ago

5c062ff9

feat(topology/instances/nnreal): add `can_lift C(X, ℝ) C(X, ℝ≥0)` (#15446)

urkud committed 3 years ago

fc2d456a

chore(logic/equiv/fin): golf, avoid `norm_num` (#15442)

urkud committed 3 years ago

1a30610a

feat(order/hom/basic): `order_iso` of `rel_iso (<) (<)` (#15432)

vihdzp committed 3 years ago

3b19e7ee

Older