leanprover-community/mathlib3

Pull Requests Commits

refactor(linear_algebra/trace): unbundle `matrix.trace` (#13712)

eric-wieser committed 3 years ago

320df450

feat(category_theory/monoidal): adjunctions in rigid categories (#13707)

kim-em committed 3 years ago

a6275694

feat(probability/martingale): the optional stopping theorem (#13630)

kex-y committed 3 years ago

fe445767

chore(category_theory/limits/cones): avoid a timeout from @[simps] (#13877)

kim-em committed 3 years ago

db0b495b

doc(data/polynomial/basic): Remove references to `polynomial.norm2` (#13847)

tb65536 committed 3 years ago

67c0e137

move(topology/algebra/floor_ring → order/floor): Move topological properties of `⌊x⌋` and `⌈x⌉` (#13824)

YaelDillies committed 3 years ago

03ed4c78

feat(linear_algebra/matrix/adjugate): `adjugate` of a diagonal matrix is diagonal (#13818)

eric-wieser committed 3 years ago

aaa167cd

feat(logic/equiv/local_equiv): add `forall_mem_target`/`exists_mem_target` (#13805)

urkud committed 3 years ago

34bbec61

feat(logic/equiv/local_equiv): add inhabited instances (#13804)

urkud committed 3 years ago

179b6c02

feat(order/zorn): add Zorn lemma on a preorder (#13803)

urkud committed 3 years ago

c1f8ac50

chore(analysis/normed_space/add_torsor): make coefficients explicit in lemmas about eventual dilations (#13796)

ocfnash committed 3 years ago

925c4738

feat(linear_algebra/finite_dimensional): of_injective (#13792)

kim-em committed 3 years ago

90b1ddba

feat(data/zmod/basic): Variant of `zmod.val_int_cast` (#13781)

tb65536 committed 3 years ago

0587eb18

feat(data/zmod/basic): `zmod 0` is infinite (#13779)

tb65536 committed 3 years ago

fd4188d7

refactor(field_theory/separable): move content about polynomial.expand earlier (#13776)

kim-em committed 3 years ago

5c914907

feat(representation_theory): Rep k G is symmetric monoidal (#13685)

kim-em committed 3 years ago

000cae16

feat(analysis/matrix): define the frobenius norm on matrices (#13497)

eric-wieser committed 3 years ago

1e385494

chore(algebraic_geometry/AffineScheme): Speed up `Spec` (#13866)

YaelDillies committed 3 years ago

3d946a3d

feat(set_theory/game/nim): Birthday of `nim` (#13873)

vihdzp committed 3 years ago

523adb38

refactor(set_theory/game/pgame): Simpler definition for `star` (#13869)

vihdzp committed 3 years ago

039543c2

feat(set_theory/surreal/basic): `<` is transitive on numeric games (#13812)

vihdzp committed 3 years ago

26e24c75

chore(logic/function/basic): don't unfold set in cantor (#13822)

digama0 committed 3 years ago

922717e8

feat(linear_algebra/tensor_product): define tensor_tensor_tensor_assoc (#13864)

antoinelab01 committed 3 years ago

afc0700e

chore(set_theory/surreal/basic): Inline instances (#13811)

vihdzp committed 3 years ago

b236cb20

feat(set_theory/pgame/impartial): `star` is impartial (#13842)

vihdzp committed 3 years ago

f0930c82

feat(data/set/function): missing mono lemmas (#13863)

sgouezel committed 3 years ago

071cb550

docs(*): Wrap some links in < … > (#13852)

nomeata committed 3 years ago

9e7c80f6

feat(set_theory/game/pgame): Add missing basic API (#13744)

vihdzp committed 3 years ago

232c15e5

feat(set_theory/game/impartial): Relabelling of impartial game is impartial (#13843)

vihdzp committed 3 years ago

51b1e118

chore(set_theory/game/impartial): golf (#13841)

vihdzp committed 3 years ago

4b92515b

Newer Older