leanprover-community/mathlib3

Pull Requests Commits

feat(linear_algebra/determinant): specialize `linear_equiv.is_unit_det` to automorphisms (#7667)

Vierkantor committed 4 years ago

f781c47e

feat(measure_theory/interval_integral): `integral_deriv_comp_mul_deriv` (#7141)

benjamindavidson committed 4 years ago

615af755

feat(algebra/char_zero): `neg_eq_self_iff` (#7916)

benjamindavidson committed 4 years ago

386962c2

docs(data/rat/denumerable): add module docstring (#7920)

YaelDillies committed 4 years ago

461b444d

feat(analysis/normed_space): nnreal.coe_nat_abs (#7911)

PatrickMassot committed 4 years ago

a853a6ae

feat(analysis/convex): add dual cone (#7738)

abentkamp committed 4 years ago

6aed9a77

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

leanprover-community-bot committed 4 years ago

fec6c8a4

feat(measure_theory/ess_sup): monotonicity of ess_sup/ess_inf w.r.t. the measure (#7917)

RemyDegenne committed 4 years ago

30045133

chore(algebra/lie/basic + classical): golf some proofs (#7903)

adomani committed 4 years ago

4fe77812

docs(set_theory/schroeder_bernstein): add module docstring (#7900)

YaelDillies committed 4 years ago

b3244884

docs(data/nat/totient): add module docstring (#7899)

YaelDillies committed 4 years ago

e971eae6

chore(measure_theory): measurability statements for coercions, coherent naming (#7854)

sgouezel committed 4 years ago

a359bd98

chore(analysis/normed_space/normed_group_hom): golf proof of normed_group_hom.bounded (#7896)

Ruben-VandeVelde committed 4 years ago

5c114586

feat(measure_theory): continuity of primitives (#7864)

PatrickMassot committed 4 years ago

2f40f351

feat(algebra/covariant_and_contravariant): API for covariant_and_contravariant (#7889)

adomani committed 4 years ago

6d2a0512

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

leanprover-community-bot committed 4 years ago

7c9643de

docs(data/nat/pairing): add module docstring (#7897)

YaelDillies committed 4 years ago

e13fd486

chore(algebra/{ordered_group, linear_ordered_comm_group_with_zero.lean}): rename one lemma, remove more @s (#7895)

adomani committed 4 years ago

2c919b08

feat(group_theory/group_action/defs): add `has_mul.to_has_scalar` and relax typeclass in `smul_mul_smul` (#7885)

ocfnash committed 4 years ago

add577d7

chore(category_theory/filtered): Adds missing instances (#7909)

adamtopaz committed 4 years ago

e0a3303f

chore(linear_algebra/quadratic_form): fix typo (#7907)

kex-y committed 4 years ago

9ad8ea3b

fix(tactic/lint): punctuation of messages (#7869)

fpvandoorn committed 4 years ago

7b7cd0a1

feat(algebra/pointwise): Dynamics of powers of a subset (#7836)

tb65536 committed 4 years ago

39073fa2

feat(topology/category/Profinite/cofiltered_clopen): Theorem about clopen sets in cofiltered limits of profinite sets (#7837)

adamtopaz committed 4 years ago

ee4fe743

feat(linear_algebra/free_module): add class module.free (#7801)

riccardobrasca committed 4 years ago

06094d56

feat(geometry/manifold): Some lemmas for smooth functions (#7752)

Nicknamen committed 4 years ago

f9935ede

chore(ring_theory/adjoin_root): speedup (#7905)

sgouezel committed 4 years ago

b7d4996e

chore(data/nat/sqrt): Alternative phrasings of data.nat.sqrt lemmas (#7748)

Smaug123 committed 4 years ago

15b24348

feat(data/polynomial): generalize `polynomial.has_scalar` to require only `distrib_mul_action` instead of `semimodule` (#7664)

eric-wieser committed 4 years ago

841dce13

feat(linear_algebra): use `finset`s to define `det` and `trace` (#7778)

Vierkantor committed 4 years ago

2016a93a

Newer Older