leanprover-community/mathlib

Pull Requests Commits

chore(linear_algebra/matrix): add fin expansions for trace and adjugate, and some trace lemmas (#9884)

eric-wieser committed 4 years ago

880c7bd4

feat(data/matrix/basic): lemmas about transpose and conj_transpose on sums and products (#9880)

eric-wieser committed 4 years ago

e808b419

chore(linear_algebra/matrix/nonsingular_inverse): replace `1 < fintype.card n` with `nontrivial n` (#9953)

eric-wieser committed 4 years ago

87fa12a7

chore(group_theory/submonoid): move a lemma to reduce imports (#9951)

urkud committed 4 years ago

0d131fe5

feat(linear_algebra/matrix/nonsingular_inverse): lemmas about adjugate (#9947)

eric-wieser committed 4 years ago

374885af

chore(analysis/normed/group/basic): make various norm instances computable (#9946)

eric-wieser committed 4 years ago

c693682f

chore(linear_algebra/matrix/nonsingular_inverse): use pi.single instead of ite (#9944)

eric-wieser committed 4 years ago

5fcbd2b9

chore(analysis/complex/circle): upgrade `exp_map_circle` to `continuous_map` (#9942)

urkud committed 4 years ago

5778df87

feat(measure_theory/measure): better `measure.restrict_singleton` (#9936)

urkud committed 4 years ago

2026a5f7

feat(analysis/special_functions/pow): Equivalent conditions for zero powers (#9897)

Smaug123 committed 4 years ago

8eb1c029

feat(*): use `ordered_sub` instead of `nat.sub` lemmas (#9855)

fpvandoorn committed 4 years ago

312db88b

refactor(linear_algebra/finite_dimensional): define finite_dimensional using module.finite (#9854)

riccardobrasca committed 4 years ago

f298c559

chore(topology/continuous_function): review API (#9950)

urkud committed 4 years ago

3d457a24

feat(linear_algebra/basic, ring_theory/ideal/basic): add span_insert (#9941)

Ruben-VandeVelde committed 4 years ago

f23354dc

refactor(data/real/ennreal): remove ordered sub simp lemmas (#9902)

fpvandoorn committed 4 years ago

26c838fc

feat(ring_theory/polynomial/cyclotomic): add lemmas about evaluation of cyclotomic polynomials at one (#9910)

alexjbest committed 4 years ago

dc1484e4

chore(group_theory/submonoid/operations): golf a few proofs (#9948)

urkud committed 4 years ago

7e532030

feat(group_theory/subgroup/basic): `normalizer_eq_top` (#9917)

tb65536 committed 4 years ago

bfcbe681

feat(group_theory/index): Second isomorphism theorem in terms of `relindex` (#9915)

tb65536 committed 4 years ago

41b90d7a

feat(group_theory/subgroup/basic): `map_subtype_le` (#9916)

tb65536 committed 4 years ago

b9260f28

chore(data/list/basic): golf a proof (#9949)

urkud committed 4 years ago

951a60ea

docs(control/traversable/lemmas): Add module docstring (#9927)

YaelDillies committed 4 years ago

264d33ec

feat(algebra/big_operators/basic): prod/sum over an empty type (#9939)

urkud committed 4 years ago

c4760b97

feat(*): a few more `fun_unique`s (#9938)

urkud committed 4 years ago

f9da68cc

chore(algebra/*/pi): add missing lemmas about function.update and set.piecewise (#9935)

eric-wieser committed 4 years ago

942e60f7

docs(control/bitraversable/instances): Add def docstrings (#9931)

YaelDillies committed 4 years ago

1e7f6b9a

docs(control/applicative): Add module docstring (#9930)

YaelDillies committed 4 years ago

5d1e8f79

docs(control/bitraversable/basic): Add defs docstrings (#9929)

YaelDillies committed 4 years ago

6f1d45dc

docs(control/traversable/equiv): Add module docstring (#9928)

YaelDillies committed 4 years ago

5642c628

feat(group_theory/subgroup/basic): Contrapositive of `card_le_one_iff_eq_bot` (#9918)

tb65536 committed 4 years ago

8c0b8c71

Newer Older