leanprover-community/mathlib3

Pull Requests Commits

we may write a semisimple module as a product of simple submodules

MadPidgeon committed 3 years ago

a3b7241c

MadPidgeon committed 3 years ago

efbcd7b1

proof of center basis

MadPidgeon committed 3 years ago

99367d36

better definitions

MadPidgeon committed 3 years ago

13034915

MadPidgeon committed 3 years ago

b1c89b18

Added text document describing the proof

pimsp committed 3 years ago

ec7e6452

chore(topology/*): rename compact_univ to is_compact_univ, and many more (#17436)

sgouezel committed 3 years ago

27929793

feat(analysis/convex/jensen): Maximum modulus principle for finsets (#17091)

YaelDillies committed 3 years ago

bfad3f45

chore(field_theory): move `polynomial.splits` to a new file (#17354)

Vierkantor committed 3 years ago

6a5a6494

chore(data/nat/basic): drop some `nat`-specific lemmas (#17400)

urkud committed 3 years ago

6b921b20

refactor(data/rat/defs): Use `int.cast` instead of `rat.of_int` (#17392)

YaelDillies committed 3 years ago

c18a48e9

refactor(topology/sheaf_condition): remove redundant constructions (#17378)

alreadydone committed 3 years ago

85d6221d

feat(category_theory/extensive): Define extensive categories (#17318)

erdOne committed 3 years ago

a6d9c65a

feat(data/finsupp/basic): add a `has_repr` instance (#17283)

eric-wieser committed 3 years ago

64444a2d

feat(analysis/normed/group/basic): `dist (a * b) b` (#17240)

YaelDillies committed 3 years ago

4a681f15

feat(algebraic_geometry/open_immersion): `is_open_immersion.lift_app` (#17186)

erdOne committed 3 years ago

ea469516

feat(algebra/module/localized_module): Add `is_localized_module.mk'`. (#17064)

erdOne committed 3 years ago

fb63d2da

feat(order/zorn): Variant for `Ici` (#17053)

YaelDillies committed 3 years ago

fc6a9d12

refactor(data/finset/prod): make arguments to `mem_diag` and `mem_off_diag` implicit (#16314)

YaelDillies committed 3 years ago

bb8b0fd0

feat(data/{multiset/dedup, finset/basic}): add some lemmas about `multiset.dedup` (#16230)

astrainfinita committed 3 years ago

937a36ee

feat(representation_theory/character): orthogonality of characters (#16043)

antoinelab01 committed 3 years ago

55b3f820

chore(*): add mathlib4 synch labels (#17417)

pechersky committed 3 years ago

16672f9c

feat(linear_algebra/affine_space/finite_dimensional): coplanarity in ambient dimension 2 (#17399)

jsm28 committed 3 years ago

0b9f6bdd

refactor(topology/vector_bundle/basic): deduplicate `trivialization` (#17359)

hrmacbeth committed 3 years ago

433802f7

feat(topology/inseparable): define `lift` and `lift₂` (#17158)

urkud committed 3 years ago

0d13c30f

feat(order/bounded_order): turn `monotone.with_bot_map` etc into `iff` lemmas (#17121)

urkud committed 3 years ago

a380a130

feat(algebra/order/hom/basic): Non-archimedean homomorphisms (#16769)

YaelDillies committed 3 years ago

d6ce021f

refactor(*): supremum of refactoring PRs #17405 #17418 #17419 #17420 #17421 #17422 #17423 #17427 #17430 (#17424)

kim-em committed 3 years ago

47b51515

chore(number_theory/divisors): golf 2 proofs (#17429)

urkud committed 3 years ago

ac4ea7ac

chore(data/polynomial/expand): golf a proof (#17428)

urkud committed 3 years ago

9619aca9

Older