leanprover-community/mathlib

Pull Requests Commits

eric-wieser committed 3 years ago

194bfeee

Merge remote-tracking branch 'origin/eric-wieser/vector-reflected' into eric-wieser/matrix-wip

eric-wieser committed 3 years ago

e4976439

eric-wieser committed 3 years ago

8d7cc4a3

feat(data/vector/basic): reflected instance for vectors

eric-wieser committed 3 years ago

17702e13

eric-wieser committed 3 years ago

667efddc

add tests, rework

eric-wieser committed 3 years ago

3a2f96ee

feat(analysis/inner_product_space): Generalize Gram-Schmidt (#14379)

abentkamp committed 3 years ago

95da6493

feat(set_theory/game/ordinal): golf `to_pgame_injective` (#14661)

vihdzp committed 3 years ago

391d1780

refactor(set_theory/game/pgame): rename and add theorems like `-y ≤ -x ↔ x ≤ y` (#14653)

vihdzp committed 3 years ago

68dc07f6

feat(data/matrix/notation): add `!ₘ[1, 2; 3, 4]` notation

eric-wieser committed 3 years ago

fd80afc4

feat(data/fintype/basic): add `card_subtype_mono` (#14645)

linesthatinterlace committed 3 years ago

a9123922

chore(topology/metric_space/basic): add `metric_space.replace_bornology` (#14638)

eric-wieser committed 3 years ago

771f2b7b

refactor(logic/equiv/basic): tweak lemmas on equivalences between `unique` types (#14605)

vihdzp committed 3 years ago

5bccb515

feat(data/polynomial/derivative): reduce assumptions (#14338)

astrainfinita committed 3 years ago

76918216

feat(dynamics/periodic_pts): Orbit under periodic function (#12976)

vihdzp committed 3 years ago

39184f40

feat(data/finite/basic): `finite` predicate (#14373)

kmill committed 3 years ago

e3dade35

chore(measure_theory): golf (#14657)

urkud committed 3 years ago

e9d25648

feat(set_theory/ordinal/basic): tweak theorems on order type of empty relation (#14650)

vihdzp committed 3 years ago

ed2cfce8

chore(analysis/special_functions/gamma): tidy some proofs (#14615)

Ruben-VandeVelde committed 3 years ago

2cf4746b

feat(ci): Add support for "notice"-level messages (#14443)

eric-wieser committed 3 years ago

3afb1fa1

feat(set_theory/ordinal/basic): better definitions for `0` and `1` (#14651)

vihdzp committed 3 years ago

6e136177

feat(set_theory/cardinal): add `cardinal.aleph_0_le_mul_iff'` (#14648)

urkud committed 3 years ago

c89d3194

feat(data/matrix): Lemmas about `vec_mul`, `mul_vec`, `dot_product`, `inv` (#14644)

abentkamp committed 3 years ago

405be36f

chore(topology/sequences): rename variables (#14631)

urkud committed 3 years ago

3e458e23

chore(set_theory/cardinal/basic): tidy lt_wf proof (#14574)

Ruben-VandeVelde committed 3 years ago

81ab992e

feat(algebra/order/ring): Binary rearrangement inequality (#14478)

YaelDillies committed 3 years ago

34a9d0df

feat(data/nat/choose/central): arity of primes in central binomial coefficients (#14017)

BoltonBailey committed 3 years ago

7fbff0f7

chore(ring_theory/unique_factorization_domain): drop simp annotation for factors_pow (#14646)

Ruben-VandeVelde committed 3 years ago

4d4de43e

feat(analysis/inner_product_space/pi_L2): Distance formula in the euclidean space (#14642)

YaelDillies committed 3 years ago

7b4680fe

feat(special_functions/integrals): exponential of complex multiple of x (#14623)

loefflerd committed 3 years ago

ac0ce64c

Older