Changelog

2022-10-01 02:05 2a543b0d
perf(algebraic_topology/simplicial_object): Speedup `simplicial_cosimplicial_augmented_equiv` (#16729) …
1 files
2022-10-01 02:05 5fefdfa1
feat(group_theory/schreier): The size of the commutator subgroup is bounded in terms of the index of the center and the number of commutators (#16679) …
2 files2 theorems
2022-09-30 23:37 7aebb349
refactor(ring_theory/polynomial/tower): review APIs (#16678) …
14 files12 theorems
2022-09-30 23:37 a753abcf
feat(linear_algebra/{basis, determinant, orientation}): determinant of `adjust_to_orientation` of a basis (#16476) …
3 files6 theorems
2022-09-30 23:37 c1a28cb2
feat(topology/semicontinuous): characterization by closed sets of semicontinuous maps to a linear order (#16442)
1 files8 theorems
2022-09-30 23:37 e4ee4e30
feat(category_theory/limits): colimits from finite colimits and filtered colimits (#16373) …
4 files20 theorems2 defs
2022-09-30 23:37 aa701d8f
feat(algebra/module/localized_module): universal property of localized module (#15559) …
2 files26 theorems
2022-09-30 21:29 866664b8
feat(data/polynomial/ring_division): add bUnion_roots_finite (#16670) …
3 files5 theorems
2022-09-30 21:28 2fb109f0
feat(analysis/inner_product/orientation, geometry/euclidean/oriented_angle): use bundled orthonormal bases (#16475) …
3 files237 theorems10 defs
2022-09-30 18:24 73afba48
refactor(analysis/normed/group/basic): Replace `normed_add_comm_group.core` with group norms (#16238) …
10 files5 theorems4 defs2 structures
2022-09-30 18:24 98c61b1e
feat(order/hom/heyting): Heyting homomorphisms (#15308) …
6 files45 theorems4 defs3 structures
2022-09-30 18:24 6e5e3f68
feat(analysis/locally_convex): the topology of a locally convex space is generated by seminorms (#15035) …
7 files14 theorems2 defs
2022-09-30 13:10 be05d53c
feat(algebra/free_monoid): add 2 lemmas (#16712)
1 files2 theorems
2022-09-30 13:10 cc967daa
feat(algebra/hom/group): `simp` lemmas for applying generic morphism coercions (#16700) …
1 files4 theorems
2022-09-30 13:10 64ad902d
refactor(algebra/order/{smul,module}): Turn lemmas around (#16696) …
3 files14 theorems
2022-09-30 13:10 a52be2a5
feat(category_theory/localization): whiskering_left_equivalence and definition of the predicate (#16646) …
3 files3 theorems7 defs
2022-09-30 13:10 c804ede6
feat(category_theory/groupoid): simplify groupoid.inv to category_theory.inv (#16624) …
1 files1 theorems1 defs
2022-09-30 13:10 3df3c617
feat(linear_algebra/quadratic_form/basic): algebraic lemmas about `bilin_form.to_quadratic_form` (#16616) …
1 files7 theorems1 defs
2022-09-30 13:10 98ed2a20
move(algebra/order/ring_lemmas): Rename file (#16520) …
2 files
2022-09-30 13:10 699c2cab
feat(analysis/convex/between): betweenness in affine spaces (#16191) …
1 files69 theorems3 defs
2022-09-30 08:02 b2a65720
feat(topology/instances/nnreal): generalize `has_continuous_smul` instance (#16713) …
1 files
2022-09-30 08:02 af90fef9
feat(data/fin): golf, add lemmas (#16711) …
2 files4 theorems
2022-09-30 08:02 d610cec7
feat(group_theory/quotient_group): `simp` lemmas for `quotient_group.map` (#16703) …
2 files5 theorems
2022-09-30 08:02 001ba509
feat(ring_theory/fractional_ideal): `simp` lemmas for `fractional_ideal.canonical_equiv` (#16702) …
1 files5 theorems
2022-09-30 08:02 acd02bbd
feat(algebra/hom/equiv): two little `simp` lemmas for `units.map_equiv` (#16701) …
1 files2 theorems
2022-09-30 08:02 3a0be826
feat(topology/sheaves): presheaf on indiscrete space is sheaf iff value at empty is terminal (#16694) …
4 files6 theorems
2022-09-30 06:01 9b1e9204
feat(topology/continuous_function/{basic, compact}): add a few missing lemmas (#16714)
2 files3 theorems
2022-09-30 06:01 667f2a62
feat(analysis/normed_space/basic): add `norm_algebra_map_nnreal` (#16709) …
1 files2 theorems
2022-09-30 03:07 07e46bcf
feat(data/fin): iff on add or sub across last-0 break (#15916)
1 files8 theorems
2022-09-30 00:01 4ed50443
feat(tactic/positivity): Extension for `finset.card` (#16637) …
2 files
2022-09-30 00:01 6fc2df65
feat(order/filter/{prod,pi}): add `filter.prod_le_prod`, `filter.pi_le_pi` etc (#16468)
4 files14 theorems
2022-09-29 21:54 ed33fcf8
feat(order/filter/*): a family of pairwise disjoint filters has a family of pairwise disjoint members (#16504)
3 files8 theorems
2022-09-29 19:48 71e28e0c
feat(topology/uniform_space/uniform_convergence_topology): bases for uniform structures of 𝔖-convergence (#14778) …
1 files
2022-09-29 16:43 c8760bde
refactor(algebra/ring/basic): replace `neg_zero'` by `neg_zero_class` instance (#16686) …
6 files1 theorems
2022-09-29 16:43 d755c086
feat(data/set/intervals/monotone): extend a monotone function on a set to a globally monotone function (#16682)
1 files2 theorems
2022-09-29 14:41 42604284
refactor(*): `inv_one_class`, `neg_zero_class` instances replacing lemmas (#16699) …
5 files4 theorems
2022-09-29 12:54 2e09d790
feat(topology/algebra/algebra): `algebra_clm` does not need a normed space or field (#16690) …
4 files7 theorems2 defs
2022-09-29 12:54 37cfab4b
feat(topology/path_connected): add five lemmas (#16501) …
1 files6 theorems
2022-09-29 10:48 a630444a
feat(analysis/analytic/isolated_zeros): the uniqueness theorem for analytic fns (#16489)
5 files16 theorems1 defs
2022-09-29 10:48 7944d185
feat(number_theory/multiplicity): lifting the exponent lemma (#8915) …
2 files25 theorems
2022-09-29 06:46 d95851bc
chore(data/finset/lattice): use more common name, fix spaces (#16336) …
3 files16 theorems
2022-09-29 01:02 78764375
refactor(data/real/ennreal): `div_inv_one_monoid` instance (#16689) …
6 files2 theorems
2022-09-29 01:02 0ec98ed0
refactor(data/real/ereal): `sub_neg_zero_monoid` instance (#16688) …
2 files3 theorems
2022-09-29 01:02 8f89631e
refactor(algebra/periodic): use `neg_zero_class` for `antiperiodic.nat_mul_eq_of_eq_zero` (#16687) …
1 files1 theorems
2022-09-29 01:02 e63a4d5e
feat(analysis/special_functions/pow): sqrt and inequalities (#16515) …
1 files5 theorems
2022-09-28 21:58 345b38d6
feat(measure_theory/measure/lebesgue): deduce that a property is almost sure from a localized version in intervals (#16684)
2 files6 theorems
2022-09-28 21:58 acc2a10b
feat(algebra/module/basic): weaken assumption (#16673)
1 files
2022-09-28 21:58 0abedaf8
feat(data/nat/parity): iterations of involutive functions (#16630)
3 files8 theorems
2022-09-28 21:58 f7698588
feat(tactic/push_neg): option for an alternate normal form of `¬ (P ∧ Q)` (#16586) …
2 files1 theorems
2022-09-28 21:58 25e7fe6b
chore(algebra/order/monoid_lemmas_zero_lt): reorder, create aliases (#16522) …
1 files14 theorems