Commits leanprover-community/mathlib

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

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