Commits leanprover-community/mathlib3

Snapshot

urkud committed 4 years ago

699c3ab7

refactor(ring_theory/unique_factorization_domain): rename unique_factorization_monoid.factors (#9503)

Ruben-VandeVelde committed 4 years ago

cff99277

feat(group_theory/quotient_group): if a quotient is trivial then the subgroup is the whole group (#9092)

CBirkbeck committed 4 years ago

18e7f914

feat(topology/basic): interior of finite intersection is intersection of interiors (#9508)

ocfnash committed 4 years ago

55c30c69

feat(analysis/normed_space/add_torsor_bases): barycentric coordinates are continuous (#9515)

ocfnash committed 4 years ago

2807d83e

feat(analysis/special_functions/exp_log): prove continuity of exp without derivatives (#9501)

RemyDegenne committed 4 years ago

7d83ff15

feat(analysis/convex/function): helper lemmas and general cleanup (#9438)

YaelDillies committed 4 years ago

5f803fae

chore(topology/*): more lemmas about `dense`/`dense_range` (#9492)

urkud committed 4 years ago

7b022774

chore(measure_theory): move, deduplicate (#9489)

urkud committed 4 years ago

c46a04a3

chore(ring_theory/ideal): some simp attributes (#9487)

PatrickMassot committed 4 years ago

a97e86a6

docs(measure_theory/integral/lebesgue): Add "Markov's inequality" to the doc string of `mul_meas_ge_le_lintegral` (#9506)

kex-y committed 4 years ago

e60dc2bb

refactor(linear_algebra/charpoly): split in two files (#9485)

riccardobrasca committed 4 years ago

110c740c

refactor(linear_algebra/free_module_pid): move linear_algebra/free_module_pid to linear_algebra/free_module/pid (#9482)

riccardobrasca committed 4 years ago

1ceebca6

feat(measure_theory/function/ae_eq_of_integral): two ennreal-valued function are a.e. equal if their integrals agree (#9372)

kex-y committed 4 years ago

fa7fdcae

feat(data/finset/interval): API for `finset.Ixx` (#9495)

YaelDillies committed 4 years ago

241aad7b

chore(src/analysis/special_functions/trigonometric/basic) : prove continuity of sin/cos/sinh/cosh without derivatives (#9502)

RemyDegenne committed 4 years ago

f3746ea6

feat(measure_theory/covering/besicovitch): the Besicovitch covering theorem (#9462)

sgouezel committed 4 years ago

e26a9e56

feat(ring_theory/algebraic_independent): algebraic independence (#9229)

ChrisHughes24 committed 4 years ago

9e54ad01

chore(algebra/star/basic): provide automorphisms in commutative rings (#9483)

eric-wieser committed 4 years ago

709b4498

feat(algebra/algebra): the range of `algebra_map (S : subalgebra R A) A` (#9450)

Vierkantor committed 4 years ago

fc7f9f3a

feat(ring_theory): quotients of a noetherian ring are noetherian (#9449)

Vierkantor committed 4 years ago

a59876f1

feat(linear_algebra/affine_space/barycentric_coords): define barycentric coordinates (#9472)

ocfnash committed 4 years ago

37f43bff

refactor(analysis/convex/caratheodory): generalize ℝ to an arbitrary linearly ordered field (#9479)

YaelDillies committed 4 years ago

06b184f9

doc(ring_theory/subring): fix docstring of `subring.center` (#9494)

ADedecker committed 4 years ago

118d45ad

refactor(analysis/convex/cone): generalize ℝ to an ordered semiring (#9481)

YaelDillies committed 4 years ago

e6f8ad79

feat(order/circular): define circular orders (#9413)

YaelDillies committed 4 years ago

05ee42cf

feat(measure_theory/function/conditional_expectation): conditional expectation on real functions equal Radon-Nikodym derivative (#9378)

kex-y committed 4 years ago

5c92eb0b

feat(probability_theory/density): define probability density functions (#9323)

kex-y committed 4 years ago

75d022bb

feat(topology/algebra): discrete group criterion (#9488)

PatrickMassot committed 4 years ago

6354fe95

feat(topology/algebra): filters bases for algebra (#9480)

PatrickMassot committed 4 years ago

a5fc0a33