Commits leanprover-community/mathlib3

feat(number_theory/number_field/basic): add integral_basis (#18474)

xroblot committed 2 years ago

641b6a82

chore(logic/equiv/basic): Generalize Type to Sort (#18543)

eric-wieser committed 2 years ago

d2d8742b

fix(data/set/semiring): fix lemma name (#18545)

eric-wieser committed 2 years ago

62e8311c

feat(field_theory/ratfunc): add lemma `coe_sub` (#18542)

faenuccio committed 2 years ago

ec80bb15

feat(ring_theory/hahn_series): add lemma neg_order (#18541)

faenuccio committed 2 years ago

a484a7d0

chore(algebra/algebra/restrict_scalars): replace `restrict_scalars_smul_def` with version that does not commit defeq-abuse. (#18540)

ocfnash committed 2 years ago

c310cfdc

fix(algebra/algebra/operations): add missing `set_semiring.down` casts (#18539)

eric-wieser committed 2 years ago

27b54c47

chore(ring_theory/finiteness): remove references to `ideal.quotient` (#18538)

jcommelin committed 2 years ago

f5edf469

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

leanprover-community-bot committed 2 years ago

832f7b91

feat(linear_algebra/free_module/pid): rename module.free_of_finite_type_torsion_free (#18537)

xroblot committed 2 years ago

f62c15c0

refactor(topology/algebra/field): drop `topological_space_units` (#18536)

urkud committed 2 years ago

c10e724b

chore(set_theory/ordinal/initial_seg): swap the names of `init` and `init'` (#18534)

astrainfinita committed 2 years ago

8da9e305

feat(linear_algebra/direct_sum/tensor_product): one-sided distributivity constructions (#18514)

eric-wieser committed 2 years ago

9b9d125b

refactor(ring_theory/ideal/operations): split quotients to a new file (#18531)

jcommelin committed 2 years ago

e7f0ddbf

chore(topology/algebra/ring): split into 2 files (#18532)

urkud committed 2 years ago

9a59dcb7

feat(data.polynomial.div): add `theorem X_pow_dvd_iff` (#18528)

faenuccio committed 2 years ago

742aa2cb

feat(analysis/complex/upper_half_plane/metric): prove that SL(2, ℝ) acts isometrically on upper half space with the hyperbolic metric (#18379)

RuizheWan committed 2 years ago

f06058e6

feat(data/finsupp/indicator, algebra/big_operators/finsupp): add some lemmas about `finsupp.indicator` (#17413)

astrainfinita committed 2 years ago

842328d9

refactor(topology/uniform_space/basic): review API (#18516)

urkud committed 2 years ago

195fcd60

perf(analysis/inner_product_space/spectrum): Squeeze simps (#18529)

YaelDillies committed 2 years ago

989433cb

doc(order/game_add): minor doc improvement (#18525)

vihdzp committed 2 years ago

fee218fb

chore(ring_theory/polynomial): squeeze a `simpa` (#18524)

Vierkantor committed 2 years ago

dfb0adb7

doc(set_theory/ordinal/exponential): improve module docstring (#18522)

vihdzp committed 2 years ago

8ee653c0

feat(analysis/convex/extreme): Extreme points of `s ×ˢ t` (#18171)

YaelDillies committed 2 years ago

c5773405

chore(combinatorics/simple_graph/connectivity): open a namespace block for `connected_component` (#18520)

bottine committed 2 years ago

e876965f

fix(algebra/star/star_alg_hom): fix typo in `star_alg_hom.coe_coe` (#18519)

j-loreaux committed 2 years ago

35882ddc

feat(combinatorics/simple_graph/basic): Simple graphs form a complete boolean algebra (#18285)

YaelDillies committed 2 years ago

c6ef6387

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

leanprover-community-bot committed 2 years ago

ee05e9ce

refactor(category theory/cofiltered_systems): rename `mittag_leffler.lean` and move `nonempty_sections_of_fintype_cofiltered_system` into new file (#18433)

bottine committed 2 years ago

8195826f

feat(combinatorics/simple_graph/regularity/bound): Local `positivity` extension (#18368)

YaelDillies committed 2 years ago

7a0dd7b2