Commits leanprover-community/mathlib

feat(geometry/euclidean/angle/unoriented/right_angle): trigonometric lemmas (#17173)

jsm28 committed 3 years ago

6bc0c198

feat(algebra/gcd_monoid): normalization and gcd are subsingletons given unique units (#17149)

Vierkantor committed 3 years ago

b30d648a

feat(measure_theory/measure/haar): add lemma `measure_theory.measure.measure_preserving_zpow` (#17137)

ocfnash committed 3 years ago

ec22570c

feat(measure_theory/integral/periodic): the volume measure on the additive circle is doubling (#17031)

ocfnash committed 3 years ago

9fb40d5a

chore(topology/sheaf_condition): is_sheaf_iff_pairwise_intersections without products (#17181)

alreadydone committed 3 years ago

20e597fb

chore(category_theory/groupoid/*) More subgroupoid lemmas (#17147)

bottine committed 3 years ago

14c11403

refactor(topology/bases): removing/adding the empty set from/to a basis (#17133)

alreadydone committed 3 years ago

dc2a9659

feat(analysis/calculus/uniform_limits_deriv): pointwise convergence out of derivative convergence on a preconnected set (#17123)

sgouezel committed 3 years ago

1a249186

feat(order/filter/ultrafilter): an ultrafilter is an atom in the lattice of filters (#17116)

urkud committed 3 years ago

c680de9e

feat(analysis/convex/side): connectedness of sides (#16938)

jsm28 committed 3 years ago

4b6fbb3e

feat(is_cyclotomic_extension/basic): add is_cyclotomic_extension.equiv (#16757)

riccardobrasca committed 3 years ago

1acf2b9a

feat(topology/sheaves/*): Notation for restriction of sections. (#16088)

erdOne committed 3 years ago

06c75afe

feat(data/nat/interval): Cauchy induction (#15880)

Shimonschlessinger committed 3 years ago

9340cc93

feat(analysis/normed_space/hahn_banach/separation): generalize to (locally convex) topological vector spaces (#16796)

ADedecker committed 3 years ago

bcf8d82b

feat({data, analysis}/complex/basic): lemmas related to `complex.partial_order` (#17170)

j-loreaux committed 3 years ago

05f9a362

feat(data/set/intervals/basic): Injectivity of half-infinite intervals (#17157)

mans0954 committed 3 years ago

438381a5

chore(data/set/pointwise): split file, reducing dependencies (#16950)

kim-em committed 3 years ago

aa329229

feat(algebra/order/floor): some nat.ceil lemmas (#16987)

alexjbest committed 3 years ago

ad7dca6a

docs(src/order/locally_finite.lean): fix a copy-paste typo (#17196)

adomani committed 3 years ago

192f43c6

feat(analysis/normed_space/star/gelfand_duality): realize the Gelfand transform as a `star_alg_equiv` (#17167)

j-loreaux committed 3 years ago

30415257

feat(algebra/group_power/order): add `pow_lt_self_of_lt_one` (#17162)

urkud committed 3 years ago

5118ae32

feat(data/fintype/basic): lemmas about `finset.univ` (#17067)

urkud committed 3 years ago

5155be47

chore(algebra/group/to_additive): move to tactic/ (#17182)

kim-em committed 3 years ago

8308d266

chore(counterexamples/zero_divisors_in_add_monoid_algebras): sort imports (#17152)

adomani committed 3 years ago

ad47ef8a

feat(topology/algebra/const_mul_action): `order_dual` instances (#17125)

YaelDillies committed 3 years ago

94a228cf

feat(topology/continuous_function/algebra): precomposition with a homeomorphism as a `star_alg_equiv` (#17166)

j-loreaux committed 3 years ago

6d37f402

fix(algebraic_geometry/morphisms/universally_closed): Fix docstring. (#17135)

erdOne committed 3 years ago

a8ae1b3f

refactor(group_theory/order_of_element): Remove `fintype` hypothesis from `pow_coprime` (#16989)

tb65536 committed 3 years ago

179dcdea

chore(analysis/inner_product_space/basic): remove `bilin_form_of_real_inner` (#15780)

mcdoll committed 3 years ago

ec3c1f27

feat(algebra/free_monoid): add `decidable_eq` instance (#17163)

urkud committed 3 years ago

43efa804