leanprover-community/mathlib

Pull Requests Commits

feat(data/fintype/basic): The cardinality of a set is at most the cardinality of the universe (#7823)

tb65536 committed 4 years ago

136e0d68

feat(algebra/lie/base_change): define extension and restriction of scalars for Lie algebras (#7808)

jcommelin committed 4 years ago

4f38062c

feat(ring_theory): define the field/algebra norm (#7636)

Vierkantor committed 4 years ago

f57f9c8b

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

leanprover-community-bot committed 4 years ago

61ca31a9

chore(algebra/algebra/subalgebra): make inf and top definitionally convenient (#7812)

eric-wieser committed 4 years ago

7a21ae17

feat(algebra/pointwise): pow_mem_pow (#7822)

tb65536 committed 4 years ago

685289c6

feat(measure_theory): add a few integration-related lemmas (#7821)

ADedecker committed 4 years ago

29d0c63d

fix(data/mv_polynomial): add missing decidable arguments (#7817)

eric-wieser committed 4 years ago

ef7c3350

docs(order/order_iso_nat): add module docstring (#7804)

YaelDillies committed 4 years ago

90ae36ea

docs(order/directed): add module docstring (#7779)

YaelDillies committed 4 years ago

4c8a627b

feat(algebra/char_p): characteristic of fraction_ring (#7703)

Jon Eugster committed 4 years ago

e3f897c2

feat(data/list/nodup): nodup.pairwise_of_forall_ne (#7587)

pechersky committed 4 years ago

ba2c0563

feat(linear_algebra/basis): use is_empty instead of ¬nonempty (#7815)

eric-wieser committed 4 years ago

7021ff9b

chore(order/(bounded,modular)_lattice): avoid classical.some in `is_complemented` instances (#7814)

eric-wieser committed 4 years ago

a4ae4adb

feat(analysis/special_functions/integrals): `integral_log` (#7732)

benjamindavidson committed 4 years ago

8b5ff9ce

feat(linear_algebra/basic): add a unique instance for linear_equiv (#7816)

eric-wieser committed 4 years ago

0b098585

feat(linear_algebra/determinant): various `basis.det` lemmas (#7669)

Vierkantor committed 4 years ago

65e3b049

feat(linear_algebra): strong rank condition implies rank condition (#7683)

kim-em committed 4 years ago

1a62bb4c

chore(data/finset|multiset|finsupp): reduce algebra/ imports (#7797)

kim-em committed 4 years ago

be183e26

feat(topology): A locally compact Hausdorff space is totally disconnected if and only if it is totally separated (#7649)

laughinggas committed 4 years ago

89928bc0

fix(tactic/lint): allow pattern def (#7785)

fpvandoorn committed 4 years ago

685adb01

feat(tactic/lift): elaborate proof with the expected type (#7739)

fpvandoorn committed 4 years ago

fa514687

feat(linear_algebra/tensor_product): define `tensor_tensor_tensor_comm` (#7724)

ocfnash committed 4 years ago

05f7e8dc

chore(data/dfinsupp): add the simp lemma coe_pre_mk (#7806)

eric-wieser committed 4 years ago

62655a23

chore(src/linear_algebra/free_module): rename file to free_module_pid (#7805)

riccardobrasca committed 4 years ago

2a93644a

chore(ring_theory/hahn_series): emb_domain_add needs only add_monoid, not semiring (#7802)

eric-wieser committed 4 years ago

fc6f9673

chore(logic/basic): add simp lemmas about exist_unique to match those about exists (#7784)

eric-wieser committed 4 years ago

54d8b94e

feat(ring_theory/tensor_product): the base change of a linear map along an algebra (#4773)

jcommelin committed 4 years ago

ef139383

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

leanprover-community-bot committed 4 years ago

b806fd43

chore(topology/bases): Rename + unprotect some lemmas (#7809)

adamtopaz committed 4 years ago

36decf5a

Newer Older