Commits leanprover-community/mathlib

Update basic.lean

astrainfinita committed 2 years ago

e5f183f2

Merge branch 'master' into FR_rel_iff

astrainfinita committed 2 years ago

b1688d5b

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

chore(set_theory/ordinal/fixed_point): style + comments (#18322)

vihdzp committed 2 years ago

0dd4319a

refactor(ring_theory): submodules that are units are finitely generated (#18510)

alreadydone committed 2 years ago

ed90a7d3

feat(set_theory/zfc/basic): range of indexed family of sets (#18296)

vihdzp committed 2 years ago

8f66c29c

chore(data/{multiset,finset}/pi): generalize from `Type` to `Sort` (#18429)

eric-wieser committed 2 years ago

4c586d29

feat(analysis/normed_space/star/continuous_functional_calculus): prove spectral permanence and construct the `continuous_functional_calculus` (#17164)

j-loreaux committed 2 years ago

e6577119

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