Commits leanprover-community/mathlib

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

split(analysis/convex/basic): split off `analysis.convex.hull` (#9477)

YaelDillies committed 4 years ago

db6d8627

chore(ring_theory/coprime): split out imports into a new file so that `is_coprime` can be used earlier. (#9403)

eric-wieser committed 4 years ago

249a015c

feat(linear_algebra/direct_sum): `submodule_is_internal_iff_independent_and_supr_eq_top` (#9214)

eric-wieser committed 4 years ago

102ce303

feat(order/locally_finite): introduce locally finite orders (#9464)

YaelDillies committed 4 years ago

9be12dd5

feat(order/basic): Antitone functions (#9119)

YaelDillies committed 4 years ago

62b8c1fa

refactor(*): replace `abs` with vertical bar notation (#8891)

mans0954 committed 4 years ago

d6bf2dd0

feat(algebraic_geometry/*): Proved Spec ⋙ Γ ≅ 𝟭 (#9416)

erdOne committed 4 years ago

c33407ae

chore(bors): bors should block on label awaiting-CI (#9478)

jcommelin committed 4 years ago

38395ed9

feat(topology/maps): for a continuous open map, preimage and interior commute (#9471)

ocfnash committed 4 years ago

5936f530

feat(linear_algebra/{bilinear,quadratic}_form): remove non-degeneracy requirement from `exists_orthogonal_basis` and Sylvester's law of inertia (#9465)

eric-wieser committed 4 years ago

265345c2

feat(data/polynomial,field_theory): `(minpoly A x).map f ≠ 1` (#9451)

Vierkantor committed 4 years ago

74457cb0

feat(algebraic_geometry/ringed_space): Define basic opens for ringed spaces. (#9358)

justus-springer committed 4 years ago

f7d7a91c

feat(data/polynomial/basic): polynomial.update (#9020)

pechersky committed 4 years ago

9235c8a3

feat(group_theory/complement): is_complement_iff_card_mul_and_disjoint (#9476)

tb65536 committed 4 years ago

e0f7d0e8

refactor(group_theory/complement): Split `complement.lean` (#9474)

tb65536 committed 4 years ago

57fa903f

feat(analysis/normed_space/lattice_ordered_group): introduce normed lattice ordered groups (#9274)

mans0954 committed 4 years ago

76ddb2bb