leanprover-community/mathlib3

Pull Requests Commits

refactor: normed spaces over rings

eric-wieser committed 2 years ago

eadf6d1c

fix(tactic/ring_exp): `X^(2^3) = X^8` not `X^6` (#18645)

Vierkantor committed 2 years ago

72e87ce0

refactor(analysis/inner_product_space/basic): do not extend normed_add_comm_group (#18583)

eric-wieser committed 2 years ago

46b633fd

fix(*): missing universe polymorphism (#18644)

eric-wieser committed 2 years ago

d11893b4

chore(data/matrix/kronecker): make the `R` argument implicit (#18624)

eric-wieser committed 2 years ago

945bc74e

feat(tactic/linear_combination): allow `linear_combination with { exponent := n }` (#15428)

robertylewis committed 2 years ago

540b766a

chore(*): add mathlib4 synchronization comments (#18642)

leanprover-community-bot committed 2 years ago

97eab485

feat(order/upper_lower/basic): The upper closure is bounded below (#18637)

YaelDillies committed 2 years ago

e9ce88cd

feat(ring_theory/mv_polynomial/ideal): lemmas about monomial ideals (#18633)

eric-wieser committed 2 years ago

72c366d0

feat(representation_theory/Rep): describe monoidal closed structure (#18148)

Amelia Livingston committed 2 years ago

0caf3701

chore(number_theory/pell): Move def. of solution type and API to beginning (#18639)

MichaelStollBayreuth committed 2 years ago

842557b6

feat(order/antichain): Antichains are order-connected (#18636)

YaelDillies committed 2 years ago

b19481de

chore(*): golf using `acc_lift₂_iff` and `well_founded_lift₂_iff` (#18526)

astrainfinita committed 2 years ago

3353f661

chore(set_theory/game/pgame): golf le and lf basic API (#18498)

astrainfinita committed 2 years ago

dc9e5ba6

chore(*): add mathlib4 synchronization comments (#18634)

leanprover-community-bot committed 2 years ago

8ef6f08f

feat(algebra/monoid_algebra): add division by a generator (#15905)

eric-wieser committed 2 years ago

57e09a12

chore(*): add mathlib4 synchronization comments (#18630)

leanprover-community-bot committed 2 years ago

c085f304

chore(analysis/calculus/cont_diff): split into two files (#18627)

sgouezel committed 2 years ago

dd6388c4

chore(*): add mathlib4 synchronization comments (#18625)

leanprover-community-bot committed 2 years ago

aa3a4205

feat(analysis/calculus/cont_diff): formula for iterated derivative of composition with linear maps (#18592)

sgouezel committed 2 years ago

4601791e

chore(*): add mathlib4 synchronization comments (#18623)

leanprover-community-bot committed 2 years ago

290a7ba0

feat(data/matrix/kronecker): lemmas about trace, det, and inv (#18610)

eric-wieser committed 2 years ago

40cc79df

refactor(linear_algebra/matrix/hermitian): golf and generalize (#18565)

eric-wieser committed 2 years ago

9abfa6f0

feat(number_theory/pell): group structure (#18568)

MichaelStollBayreuth committed 2 years ago

7ec29468

chore(linear_algebra/affine_space/affine_subspace) add set_like instance (#18622)

mcdoll committed 2 years ago

e96bdfbd

chore(analysis/inner_product_space/basic): explicit `𝕜` argument for `innerₛₗ` and `innerSL` (#18613)

eric-wieser committed 2 years ago

c78cad35

chore(*): add mathlib4 synchronization comments (#18621)

leanprover-community-bot committed 2 years ago

1dac236e

feat(algebra/group/commute): `div` lemmas (#18607)

YaelDillies committed 2 years ago

05101c3d

chore(linear_algebra/free_module/basic): golf a proof (#18615)

eric-wieser committed 2 years ago

4e7e7009

perf(group_theory/torsion): Speedup `torsion_mul_equiv` (#18614)

YaelDillies committed 2 years ago

1f4705cc

Older