leanprover-community/mathlib

Pull Requests Commits

refactor(set_theory/game/*): remove `relabelling`

astrainfinita committed 2 years ago

e91c4253

astrainfinita committed 2 years ago

178d7013

no they are lemmas

astrainfinita committed 2 years ago

a0da9565

`one_mul` `mul_one`

astrainfinita committed 2 years ago

ec638b9e

astrainfinita committed 2 years ago

307fe760

astrainfinita committed 2 years ago

371fefb3

astrainfinita committed 2 years ago

f61ce93f

`identical_zero` `identical.sub`

astrainfinita committed 2 years ago

d2e5ec35

astrainfinita committed 2 years ago

415aea22

astrainfinita committed 2 years ago

fe396470

docs, protected

astrainfinita committed 2 years ago

1b3d193b

feat(set_theory/game/pgame): define `pgame.identical`

astrainfinita committed 2 years ago

855fd1cd

feat(combinatorics/simple_graph/hom): add basic definitions and lemmas for finite subgraphs (#16382)

jchoules committed 2 years ago

da083dad

feat(algebra/dual_quaternion): two equivalent ways to construct the dual quaternions (#18383)

eric-wieser committed 2 years ago

536c256e

chore(data/set/semiring): add an `idem_semiring` instance (#18449)

eric-wieser committed 2 years ago

a51ce549

feat(set_theory/zfc/basic): induction principle for sets (#18324)

vihdzp committed 2 years ago

d7feae34

feat(order/game_add): `sym2.game_add` (#18287)

vihdzp committed 2 years ago

7b1d4abc

chore(geometry/manifold/vector_bundle): golf (#18509)

urkud committed 2 years ago

87ecf961

refactor(topology/*): add `uniform_space.of_fun`, use it (#18495)

urkud committed 2 years ago

e1a7bdeb

fix(geometry/manifold/vector_bundle): fix timeout (#18507)

fpvandoorn committed 2 years ago

23a3e7d9

feat(data/list/basic): missing lemmas about `list.enum` (#18489)

eric-wieser committed 2 years ago

9da1b353

refactor(number_theory/pell): Small golf using `int.eq_of_mul_eq_one` (#18505)

tb65536 committed 2 years ago

35c1956c

feat(algebra/order/ring/canonical): add `canonically_ordered_comm_semiring.to_ordered_comm_monoid` (#18504)

urkud committed 2 years ago

824f9ae9

fix(data/finmap): `finmap.all` should not always be `ff` (#18432)

eric-wieser committed 2 years ago

c3fc15b2

feat(geometry/euclidean/angle/unoriented): sine & cosine angle lemmas (#18222)

JovanGerb committed 2 years ago

aedfb56f

feat(linear_algebra/bilinear_form/tensor_product): tensor product of bilinear forms (#18211)

eric-wieser committed 2 years ago

f91d3736

feat(data/nat/multiplicity): rename `nat.multiplicity_choose_prime_pow`, add lemmas (#18183)

urkud committed 2 years ago

114ff8a4

chore(data/real/ennreal): drop some lemmas (#18501)

urkud committed 2 years ago

57ac39bd

feat(algebraic_geometry/elliptic_curve/point): define homomorphism induced by base change (#18493)

Multramate committed 2 years ago

03994e05

feat(data/int/units): If `z * w = 1`, then `z = w` (#18499)

tb65536 committed 2 years ago

45a1ada0

Older