leanprover-community/mathlib

Pull Requests Commits

abentkamp committed 3 years ago

8278c24b

abentkamp committed 3 years ago

4e37ea04

gram_schmidt_orthonormal'

abentkamp committed 3 years ago

8d9fbacf

generalize more

abentkamp committed 3 years ago

21fc29d4

generalize gram_schmidt_ne_zero

abentkamp committed 3 years ago

1eacc67b

refactor(set_theory/cardinal/*): add `succ_order` instance, rename `succ` lemmas (#14244)

vihdzp committed 3 years ago

a6b90beb

feat(linear_algebra/trace): trace of projection maps (#14165)

antoinelab01 committed 3 years ago

113f7e42

feat(data/zmod/basic): If the orbit is finite, then the minimal period is positive (#14201)

tb65536 committed 3 years ago

1983e40a

chore(measure_theory/integral/lebesgue): golf some proofs (#14256)

urkud committed 3 years ago

846ed9f2

feat(set_theory/game/pgame): Tweak `pgame.add` API (#13611)

vihdzp committed 3 years ago

180d9751

feat(algebra/algebra/operations): add right induction principles for power membership (#14219)

eric-wieser committed 3 years ago

1483eca1

feat(linear_algebra/trace): trace of prod_map (#13872)

antoinelab01 committed 3 years ago

1e011e3f

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

leanprover-community-bot committed 3 years ago

735fbe05

feat(data/polynomial/mirror): `mirror_eq_iff` (#14238)

tb65536 committed 3 years ago

a5878bbe

refactor(category_theory/discrete): make discrete irreducible (#13762)

kim-em committed 3 years ago

c9c9fa15

feat (algebra/group/prod): Showing that embed_product is injective (#14247)

laughinggas committed 3 years ago

5cf7a1c5

feat(algebra/group/conj): instances + misc (#13943)

ericrbg committed 3 years ago

3c6f16c3

chore(*) : `zero_dvd_iff.1` → `eq_zero_of_zero_dvd` (#14241)

vihdzp committed 3 years ago

c8f2a1f4

feat(topology/locally_constant): Characteristic functions on clopen sets are locally constant (#11708)

laughinggas committed 3 years ago

ffe70020

chore(linear_algebra/quadratic_form/basic): remove redundant fields (#14246)

eric-wieser committed 3 years ago

d403cadd

doc(tactic/lint/type_classes): Fix small typo (#14242)

vihdzp committed 3 years ago

218d66a1

feat(group_theory/quotient_group): properties of quotients of homomorphisms and equivalences (#13046)

Multramate committed 3 years ago

e29d9110

feat(order/complete_lattice): add `Sup_diff_singleton_bot` etc (#14205)

urkud committed 3 years ago

18624efa

feat(analysis/normed_space/pi_Lp): add missing nnnorm lemmas (#14221)

eric-wieser committed 3 years ago

6906b6f7

docs(category_theory/*): the last missing module docs (#14237)

kim-em committed 3 years ago

ea3009f6

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

leanprover-community-bot committed 3 years ago

923a14da

refactor(set_theory/game/pgame): Rename `le_def_lf` → `le_iff_forall_lf` (#14206)

vihdzp committed 3 years ago

83285b24

feat(topology/algebra/module/basic): add `continuous_linear_map.apply_module` (#14223)

eric-wieser committed 3 years ago

cc74bcbd

feat(category_theory/limits): (co/bi)products over types with a unique term (#14191)

kim-em committed 3 years ago

76f9f454

doc(deprecated/*): all deprecated files now lint (#14233)

kbuzzard committed 3 years ago

c42cff11

Older