leanprover-community/mathlib

Pull Requests Commits

probability notation

YaelDillies committed 2 years ago

7ddf49bc

move to archive

YaelDillies committed 2 years ago

22ebbd09

simplify down to three variables

YaelDillies committed 2 years ago

3a577c48

YaelDillies committed 2 years ago

d72f6f07

fix measure_theory.function.strongly_measurable.basic

YaelDillies committed 2 years ago

a09c7b1f

YaelDillies committed 2 years ago

684a0b5c

YaelDillies committed 2 years ago

db19cec0

start of a cleanup

YaelDillies committed 2 years ago

4e100152

Merge remote-tracking branch 'origin/master' into bell_pr

YaelDillies committed 2 years ago

d980e51e

feat(ring_theory/dedekind_domain/finite_adele_ring): add finite_adele_ring (#14249)

mariainesdff committed 2 years ago

a8e7ac80

chore(data/real/nnreal): drop some lemmas (#18492)

urkud committed 2 years ago

b2ff9a3d

feat(algebra/quaternion): add `quaternion.im` for the skew-adjoint part (#18456)

eric-wieser committed 2 years ago

d90149e9

refactor(data/real/ereal): add a two-argument induction principle (#18481)

eric-wieser committed 2 years ago

634284e7

feat(geometry/manifold/cont_mdiff): local structomorphisms of `cont_diff_groupoid` (#17291)

hrmacbeth committed 2 years ago

8e57ff9a

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

leanprover-community-bot committed 2 years ago

ef7acf40

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

Older