leanprover-community/mathlib3

Pull Requests Commits

awainverse committed 2 years ago

96814036

feat(analysis/normed_space/star/multiplier): construct the multiplier algebra of a C*-algebra (#15869)

j-loreaux committed 2 years ago

651f93df

feat(topology/uniform_space/cauchy): `mul_opposite X` is complete when `X` is (#18471)

eric-wieser committed 2 years ago

22131150

refactor(algebra/{dual_number,triv_sq_zero_ext}): support non-commutative rings (#18384)

eric-wieser committed 2 years ago

b8d2eaa6

feat(model_theory/order): Renames and generalizes notation about ordered structures (#17870)

awainverse committed 2 years ago

1ed3a113

chore(category_theory/comma): removed obviously tactic for data fields (#18440)

joelriou committed 2 years ago

8a318021

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

leanprover-community-bot committed 2 years ago

296726c9

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

leanprover-community-bot committed 2 years ago

3dadefa3

feat(topology/continuous_function): some lemmas spun off from #18392 (#18465)

loefflerd committed 2 years ago

6efec6bb

feat(docs): allow deeper nesting within undergrad.yaml (#18407)

eric-wieser committed 2 years ago

3ade05ac

fix(group_theory/nielsen_schreier): fix typo (#18483)

ChrisHughes24 committed 2 years ago

1bda4fc5

feat(analysis/normed): `mul_opposite X` inherits the same norm as `X`. (#18470)

eric-wieser committed 2 years ago

335232c7

feat(data/set): add lemmas about `powerset` of `insert` and `singleton` (#18356)

joneugster committed 2 years ago

45501380

feat(linear_algebra/affine_space/affine_subspace): `⊥ < affine_span k s ↔ s.nonempty` (#18170)

YaelDillies committed 2 years ago

b875cbb7

feat(data/real/ereal): positive covariance typeclasses (#18157)

astrainfinita committed 2 years ago

464e1ddc

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

leanprover-community-bot committed 2 years ago

23aa88e3

refactor(linear_algebra/bilinear_map): move lemmas about `basis` to a new file. (#18468)

eric-wieser committed 2 years ago

87c54600

feat(data/prod): bijectivity of prod.map (#18446)

eric-wieser committed 2 years ago

bd9851ca

chore(linear_algebra/prod): add a missing lemma (#18445)

eric-wieser committed 2 years ago

57a30493

chore(number_theory/sum_four_squares): squeeze simps (#18467)

eric-wieser committed 2 years ago

f434b205

feat(probability/kernel/basic): add kernel.with_density (#18463)

RemyDegenne committed 2 years ago

31a8a276

feat(algebra/quandle): Unital shelves (#17839)

kisonecat committed 2 years ago

28aa996f

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

leanprover-community-bot committed 2 years ago

e97cf15c

chore(number_theory/sum_four_squares): squeeze simps (#18461)

eric-wieser committed 2 years ago

297619ec

doc(algebra/continued_fractions/*): TeXify docstrings (#18459)

MichaelStollBayreuth committed 2 years ago

2738d2ca

fix(ring_theory/derivation): speed up a slow definition (#18457)

eric-wieser committed 2 years ago

0324bd3f

feat(measure_theory/integral): break up integrals into sums (#18425)

loefflerd committed 2 years ago

e7286cac

ci(.github/workflows): lint for formatting issues in references.bib (#16614)

Ruben-VandeVelde committed 2 years ago

973ed779

fix(.github/workflows): try a fix for review bodies (#18455)

alexjbest committed 2 years ago

1df9a174

feat(topology/algebra/order/upper_lower): The closure of an upper set (#16975)

YaelDillies committed 2 years ago

4330aae2

Older