leanprover-community/mathlib3

Pull Requests Commits

j-loreaux committed 3 years ago

61ea6fd4

j-loreaux committed 3 years ago

bad493b4

move non_unital_ring_hom_class instance

j-loreaux committed 3 years ago

8441c112

add `norm_one_class`

j-loreaux committed 3 years ago

8aec967d

add `normed_field.induced` and `normed_algebra.induced`

j-loreaux committed 3 years ago

f6c4e361

fix `zero_at_infty`

j-loreaux committed 3 years ago

Verified eeb93e4e

add `normed_space.induced`

j-loreaux committed 3 years ago

Verified c73a3f39

add more induced

j-loreaux committed 3 years ago

Verified c262cbb4

make some changes

j-loreaux committed 3 years ago

dd18380c

fix zero_at_infty

j-loreaux committed 3 years ago

acd1151f

generalize `(semi)normed_add_comm_group.induced` to hom class

j-loreaux committed 3 years ago

Verified f3eaa34d

feat(data/zmod/quotient): Version of `order_eq_card_zpowers` in terms of `nat.card` without a `fintype`/`finite` assumption (#16175)

tb65536 committed 3 years ago

3d0bb870

feat(topology/uniform_space/uniform_convergence): tendsto_uniformly_on_filter (#15871)

khwilson committed 3 years ago

b6258037

docs(algebra/field/basic): fix typo (#16241)

jcommelin committed 3 years ago

36e16da1

chore(scripts): update nolints.txt (#16244)

leanprover-community-bot committed 3 years ago

b6931e1c

feat(tactic/tauto): add support for `¬_ ≠ _` (#16232)

adomani committed 3 years ago

c5be877a

chore(analysis/normed_space/star/*): migrate use of `a ∈ self_adjoint A` to `is_self_adjoint a` (#16212)

j-loreaux committed 3 years ago

fec8ffec

feat(analysis/convex/cone): add `inner_dual_cone_of_inner_dual_cone_eq_self` for nonempty, closed, convex cones (#15637)

apurvnakade committed 3 years ago

42d64072

feat(algebra/group_with_zero): add `eq_on_inv₀` (#16222)

urkud committed 3 years ago

bd12701e

chore(algebra/order/{module, smul}): Move to the correct spot (#16131)

YaelDillies committed 3 years ago

2ca1b571

refactor(order/well_founded_set): golf, review API (#11303)

urkud committed 3 years ago

4b440bb0

feat(geometry/euclidean/oriented_angle): angles equal to 0 or π (#16229)

jsm28 committed 3 years ago

f1f166b2

feat(topology/separation): add `eq_on_closure₂` (#16206)

urkud committed 3 years ago

a51c2fd2

refactor(algebra/order/{monoid_lemmas_zero_lt + ring} + crumbs) remove duplicate lemmas (#16189)

adomani committed 3 years ago

62740866

feat(category_theory/strong_epi): various results about strong_epi (#16182)

joelriou committed 3 years ago

093c5036

split(analysis/normed/group/seminorm): Split off `analysis.seminorm` (#16152)

YaelDillies committed 3 years ago

f5afe205

feat(data/polynomial/module): Some api for `polynomial_module`. (#16126)

erdOne committed 3 years ago

81afa2cb

feat(algebraic_topology/dold_kan): the normalized Moore complex is a direct factor of the alternating face map complex (#16071)

joelriou committed 3 years ago

fc5b2d2e

feat(category_theory/currying): bifunctor version of whiskering_right (#15504)

antoinelab01 committed 3 years ago

0be7214f

feat(order/heyting_algebra): Heyting algebras (#15305)

YaelDillies committed 3 years ago

96ed4226

Older