gistfile1.txt

# Unneeded in algebra.algebra.subalgebra.pointwise
ring_theory.subring.pointwise

# Unneeded in algebra.associated
algebra.invertible

# Unneeded in algebra.big_operators.associated
algebra.big_operators.finsupp

# Unneeded in algebra.big_operators.multiset
algebra.group_with_zero.power

# Unneeded in algebra.big_operators.norm_num
data.finset.interval
data.nat.interval

# Unneeded in algebra.category.FinVect
linear_algebra.tensor_product_basis

# Unneeded in algebra.category.Group.colimits
category_theory.limits.concrete_category
category_theory.limits.shapes.concrete_category

# Unneeded in algebra.category.Group.epi_mono
category_theory.epi_mono

# Unneeded in algebra.category.Group.images
category_theory.limits.types

# Unneeded in algebra.category.Group.injective
algebra.category.Group.Z_Module_equivalence

# Unneeded in algebra.category.Group.limits
category_theory.limits.concrete_category
category_theory.limits.shapes.concrete_category

# Unneeded in algebra.category.Group.zero
category_theory.limits.shapes.zero_morphisms

# Unneeded in algebra.category.GroupWithZero
algebra.category.Group.basic

# Unneeded in algebra.category.Module.algebra
algebra.category.Module.monoidal

# Unneeded in algebra.category.Module.basic
category_theory.limits.shapes.kernels

# Unneeded in algebra.category.Module.biproducts
algebra.category.Module.limits

# Unneeded in algebra.category.Module.colimits
category_theory.limits.concrete_category
category_theory.limits.shapes.kernels
group_theory.quotient_group

# Unneeded in algebra.category.Module.epi_mono
algebra.category.Group.epi_mono

# Unneeded in algebra.category.Module.images
category_theory.limits.types

# Unneeded in algebra.category.Module.kernels
category_theory.limits.concrete_category

# Unneeded in algebra.category.Module.products
algebra.category.Module.epi_mono

# Unneeded in algebra.category.Module.simple
algebra.category.Module.abelian

# Unneeded in algebra.category.Module.subobject
category_theory.limits.concrete_category

# Unneeded in algebra.category.Mon.colimits
category_theory.limits.concrete_category

# Unneeded in algebra.category.Mon.filtered_colimits
category_theory.limits.concrete_category

# Unneeded in algebra.category.Ring.basic
category_theory.concrete_category.reflects_isomorphisms

# Unneeded in algebra.category.Ring.colimits
category_theory.limits.concrete_category

# Unneeded in algebra.category.Ring.constructions
algebra.category.Ring.colimits
category_theory.limits.preserves.limits

# Unneeded in algebra.char_p.basic
data.zmod.defs

# Unneeded in algebra.char_p.exp_char
algebra.char_zero

# Unneeded in algebra.char_p.invertible
algebra.field.basic

# Unneeded in algebra.char_p.local_ring
data.nat.factorization.prime_pow

# Unneeded in algebra.char_p.mixed_char_zero
algebra.char_p.algebra
data.pnat.basic

# Unneeded in algebra.char_zero.quotient
algebra.char_zero

# Unneeded in algebra.continued_fractions.computation.terminates_iff_rat
algebra.order.archimedean

# Unneeded in algebra.direct_sum.basic
group_theory.subgroup.basic

# Unneeded in algebra.direct_sum.ring
algebra.big_operators.pi
group_theory.subgroup.basic

# Unneeded in algebra.divisibility.units
algebra.hom.units

# Unneeded in algebra.euclidean_domain.basic
algebra.field.defs

# Unneeded in algebra.euclidean_domain.defs
algebra.field.defs
algebra.hom.group
algebra.opposites
algebra.order.monoid.lemmas

# Unneeded in algebra.field.basic
algebra.ring.basic
data.rat.defs

# Unneeded in algebra.gcd_monoid.integrally_closed
ring_theory.polynomial.scale_roots

# Unneeded in algebra.gcd_monoid.multiset
data.multiset.lattice

# Unneeded in algebra.geom_sum
algebra.group_with_zero.power

# Unneeded in algebra.group.prod
algebra.hom.equiv.units.group_with_zero

# Unneeded in algebra.group.units
logic.nontrivial

# Unneeded in algebra.group_power.ring
data.nat.order.lemmas

# Unneeded in algebra.hom.centroid
algebra.group.pi

# Unneeded in algebra.hom.iterate
algebra.group_power.basic

# Unneeded in algebra.hom.units
algebra.group.commute

# Unneeded in algebra.homology.Module
algebra.homology.homotopy

# Unneeded in algebra.invertible
algebra.ring.basic

# Unneeded in algebra.jordan.basic
algebra.ring.basic

# Unneeded in algebra.lie.cartan_matrix
data.matrix.notation

# Unneeded in algebra.module.injective
algebra.category.Module.abelian

# Unneeded in algebra.module.linear_map
algebra.star.basic

# Unneeded in algebra.module.localized_module
ring_theory.ideal.operations

# Unneeded in algebra.module.submodule.pointwise
group_theory.subgroup.pointwise

# Unneeded in algebra.order.group.abs
algebra.order.monoid.canonical.defs

# Unneeded in algebra.order.group.densely_ordered
algebra.order.group.instances

# Unneeded in algebra.order.hom.basic
algebra.hom.group
algebra.order.with_zero
order.hom.basic

# Unneeded in algebra.order.hom.monoid
algebra.order.with_zero

# Unneeded in algebra.order.monoid.basic
algebra.group.units

# Unneeded in algebra.order.monoid.canonical.defs
order.min_max

# Unneeded in algebra.order.monoid.min_max
algebra.order.monoid.defs

# Unneeded in algebra.order.monoid.units
algebra.order.monoid.defs

# Unneeded in algebra.order.monoid.with_top
algebra.order.monoid.with_zero

# Unneeded in algebra.order.positive.ring
algebra.order.ring.inj_surj

# Unneeded in algebra.order.ring.defs
algebra.order.sub.defs

# Unneeded in algebra.order.ring.inj_surj
algebra.order.group.inj_surj

# Unneeded in algebra.order.smul
data.set.pointwise.basic

# Unneeded in algebra.order.sub.defs
algebra.order.monoid.defs
algebra.ring.defs

# Unneeded in algebra.order.to_interval_mod
algebra.periodic

# Unneeded in algebra.order.with_zero
algebra.order.group.type_tags

# Unneeded in algebra.quandle
data.zmod.basic

# Unneeded in algebra.quotient
data.set_like.basic

# Unneeded in algebra.regular.pow
algebra.group_power.basic

# Unneeded in algebra.ring.boolean_ring
order.heyting.hom

# Unneeded in algebra.ring.divisibility
algebra.ring.basic

# Unneeded in algebra.ring.fin
algebra.ring.pi
algebra.ring.prod

# Unneeded in algebra.ring.idempotents
algebra.ring.basic

# Unneeded in algebra.ring.prod
algebra.order.group.prod

# Unneeded in algebra.ring.regular
algebra.ring.basic

# Unneeded in algebra.ring.semiconj
algebra.ring.basic

# Unneeded in algebra.ring.units
algebra.ring.basic

# Unneeded in algebra.star.chsh
analysis.special_functions.pow

# Unneeded in algebra.star.pi
algebra.module.pi

# Unneeded in algebra.star.prod
algebra.module.prod

# Unneeded in algebra.star.unitary
group_theory.submonoid.membership

# Unneeded in algebra.support
algebra.module.pi

# Unneeded in algebra.tropical.basic
algebra.order.group.min_max

# Unneeded in algebra.tropical.big_operators
algebra.tropical.lattice

# Unneeded in algebraic_geometry.limits
category_theory.limits.constructions.equalizers
category_theory.limits.constructions.finite_products_of_binary_products

# Unneeded in algebraic_geometry.morphisms.finite_type
algebraic_geometry.morphisms.quasi_compact

# Unneeded in algebraic_geometry.presheafed_space.has_colimits
category_theory.limits.concrete_category

# Unneeded in algebraic_geometry.projective_spectrum.topology
topology.category.Top.default

# Unneeded in algebraic_geometry.properties
category_theory.limits.constructions.binary_products
ring_theory.integral_domain

# Unneeded in algebraic_topology.dold_kan.degeneracies
algebraic_topology.split_simplicial_object

# Unneeded in algebraic_topology.dold_kan.faces
data.nat.parity

# Unneeded in algebraic_topology.dold_kan.homotopies
algebraic_topology.dold_kan.notations

# Unneeded in algebraic_topology.fundamental_groupoid.fundamental_group
category_theory.category.Groupoid

# Unneeded in algebraic_topology.fundamental_groupoid.product
category_theory.limits.preserves.shapes.products

# Unneeded in algebraic_topology.fundamental_groupoid.punit
algebraic_topology.fundamental_groupoid.induced_maps

# Unneeded in analysis.analytic.isolated_zeros
analysis.complex.basic

# Unneeded in analysis.bounded_variation
data.set.intervals.monotone

# Unneeded in analysis.box_integral.partition.additive
data.set.intervals.proj_Icc

# Unneeded in analysis.calculus.taylor
measure_theory.integral.interval_integral

# Unneeded in analysis.complex.abs_max
analysis.convex.integral

# Unneeded in analysis.complex.open_mapping
topology.algebra.field

# Unneeded in analysis.complex.unit_disc.basic
group_theory.subsemigroup.membership

# Unneeded in analysis.convex.simplicial_complex.basic
analysis.convex.topology

# Unneeded in analysis.inner_product_space.basic
analysis.normed_space.banach
linear_algebra.sesquilinear_form

# Unneeded in analysis.inner_product_space.gram_schmidt_ortho
order.well_founded_set

# Unneeded in analysis.inner_product_space.positive
analysis.inner_product_space.l2_space

# Unneeded in analysis.inner_product_space.projection
analysis.inner_product_space.symmetric

# Unneeded in analysis.locally_convex.balanced_core_hull
order.closure

# Unneeded in analysis.locally_convex.basic
analysis.normed.order.basic
analysis.normed.order.lattice

# Unneeded in analysis.locally_convex.continuous_of_bounded
analysis.normed_space.is_R_or_C

# Unneeded in analysis.locally_convex.polar
analysis.convex.basic

# Unneeded in analysis.normed.group.add_torsor
linear_algebra.affine_space.midpoint

# Unneeded in analysis.normed.group.basic
algebra.module.ulift

# Unneeded in analysis.normed.order.basic
analysis.normed_space.basic

# Unneeded in analysis.normed.ring.seminorm
analysis.seminorm

# Unneeded in analysis.normed_space.M_structure
analysis.normed_space.basic

# Unneeded in analysis.normed_space.add_torsor_bases
analysis.normed_space.banach
linear_algebra.affine_space.finite_dimensional

# Unneeded in analysis.normed_space.affine_isometry
analysis.normed_space.add_torsor

# Unneeded in analysis.normed_space.basic
analysis.normed.group.infinite_sum
data.matrix.basic
topology.sequences

# Unneeded in analysis.normed_space.continuous_affine_map
analysis.normed_space.add_torsor

# Unneeded in analysis.normed_space.exponential
analysis.specific_limits.basic

# Unneeded in analysis.normed_space.hahn_banach.separation
analysis.locally_convex.with_seminorms

# Unneeded in analysis.normed_space.int
analysis.normed_space.basic

# Unneeded in analysis.normed_space.lp_space
analysis.normed.group.pointwise

# Unneeded in analysis.normed_space.operator_norm
analysis.normed_space.riesz_lemma

# Unneeded in analysis.normed_space.spectrum
analysis.special_functions.exponential

# Unneeded in analysis.normed_space.star.exponential
algebra.star.module
analysis.normed_space.star.basic
analysis.special_functions.exponential

# Unneeded in analysis.normed_space.star.spectrum
algebra.star.module

# Unneeded in analysis.schwartz_space
analysis.complex.basic
analysis.locally_convex.continuous_of_bounded

# Unneeded in analysis.seminorm
data.real.sqrt
topology.algebra.filter_basis

# Unneeded in analysis.special_functions.japanese_bracket
measure_theory.integral.integral_eq_improper

# Unneeded in analysis.special_functions.trigonometric.bounds
analysis.special_functions.trigonometric.deriv

# Unneeded in analysis.sum_integral_comparisons
algebra.order.floor

# Unneeded in category_theory.Fintype
data.fin.basic

# Unneeded in category_theory.abelian.basic
category_theory.limits.constructions.epi_mono

# Unneeded in category_theory.abelian.exact
category_theory.limits.constructions.finite_products_of_binary_products

# Unneeded in category_theory.abelian.ext
algebra.category.Group.basic

# Unneeded in category_theory.abelian.opposite
category_theory.limits.constructions.limits_of_products_and_equalizers

# Unneeded in category_theory.abelian.pseudoelements
algebra.category.Module.abelian

# Unneeded in category_theory.abelian.subobject
category_theory.abelian.opposite

# Unneeded in category_theory.abelian.transfer
category_theory.preadditive.additive_functor

# Unneeded in category_theory.adjunction.whiskering
category_theory.adjunction.default

# Unneeded in category_theory.bicategory.coherence_tactic
category_theory.bicategory.coherence

# Unneeded in category_theory.bicategory.single_obj
category_theory.monoidal.functorial

# Unneeded in category_theory.closed.zero
category_theory.limits.shapes.zero_morphisms

# Unneeded in category_theory.connected_components
category_theory.punit

# Unneeded in category_theory.endofunctor.algebra
category_theory.limits.final

# Unneeded in category_theory.epi_mono
category_theory.adjunction.basic

# Unneeded in category_theory.filtered
order.bounded_order

# Unneeded in category_theory.functor.flat
category_theory.limits.preserves.shapes.equalizers

# Unneeded in category_theory.functor.functorial
category_theory.functor.default

# Unneeded in category_theory.groupoid.basic
category_theory.is_connected

# Unneeded in category_theory.groupoid.free_groupoid
logic.relation

# Unneeded in category_theory.groupoid.subgroupoid
algebra.hom.equiv.basic
algebra.hom.group
combinatorics.quiver.connected_component

# Unneeded in category_theory.idempotents.functor_extension
category_theory.natural_isomorphism

# Unneeded in category_theory.isomorphism
category_theory.functor.default

# Unneeded in category_theory.limits.bicones
category_theory.structured_arrow

# Unneeded in category_theory.limits.comma
category_theory.limits.preserves.finite
category_theory.limits.shapes.finite_limits

# Unneeded in category_theory.limits.concrete_category
category_theory.concrete_category.elementwise

# Unneeded in category_theory.limits.constructions.finite_products_of_binary_products
category_theory.pempty

# Unneeded in category_theory.limits.mono_coprod
category_theory.limits.types
category_theory.morphism_property

# Unneeded in category_theory.limits.preserves.shapes.biproducts
category_theory.limits.preserves.shapes.binary_products
category_theory.limits.preserves.shapes.products

# Unneeded in category_theory.limits.preserves.shapes.kernels
category_theory.limits.preserves.shapes.equalizers

# Unneeded in category_theory.limits.presheaf
category_theory.limits.preserves.limits

# Unneeded in category_theory.limits.shapes.biproducts
algebra.group.ext
category_theory.preadditive.default

# Unneeded in category_theory.limits.shapes.comm_sq
category_theory.limits.preserves.shapes.pullbacks

# Unneeded in category_theory.limits.shapes.diagonal
category_theory.limits.shapes.kernel_pair

# Unneeded in category_theory.limits.shapes.finite_limits
category_theory.limits.shapes.pullbacks

# Unneeded in category_theory.limits.shapes.finite_products
category_theory.limits.shapes.binary_products
category_theory.limits.shapes.terminal

# Unneeded in category_theory.limits.shapes.multiequalizer
category_theory.adjunction.default

# Unneeded in category_theory.limits.shapes.strict_initial
category_theory.epi_mono

# Unneeded in category_theory.limits.shapes.wide_equalizers
category_theory.epi_mono

# Unneeded in category_theory.limits.shapes.zero_objects
category_theory.isomorphism_classes
category_theory.limits.shapes.images
category_theory.limits.shapes.products

# Unneeded in category_theory.linear.default
linear_algebra.basic

# Unneeded in category_theory.linear.yoneda
category_theory.preadditive.yoneda

# Unneeded in category_theory.monad.equiv_mon
category_theory.category.Cat

# Unneeded in category_theory.monad.limits
category_theory.limits.preserves.shapes.terminal

# Unneeded in category_theory.monoidal.coherence
category_theory.monoidal.free.coherence

# Unneeded in category_theory.monoidal.of_chosen_finite_products
category_theory.limits.shapes.terminal

# Unneeded in category_theory.monoidal.skeleton
category_theory.monoidal.functor

# Unneeded in category_theory.monoidal.subcategory
category_theory.concrete_category.basic

# Unneeded in category_theory.natural_transformation
category_theory.functor.default

# Unneeded in category_theory.preadditive.left_exact
category_theory.abelian.opposite

# Unneeded in category_theory.quotient
category_theory.equivalence

# Unneeded in category_theory.sigma.basic
data.sigma.basic

# Unneeded in category_theory.sites.adjunction
category_theory.sites.compatible_sheafification

# Unneeded in category_theory.sites.compatible_plus
category_theory.sites.sheafification

# Unneeded in category_theory.sites.plus
category_theory.preadditive.additive_functor

# Unneeded in category_theory.sites.sheaf_of_types
category_theory.full_subcategory

# Unneeded in category_theory.sites.subsheaf
category_theory.limits.constructions.epi_mono
category_theory.sites.compatible_sheafification

# Unneeded in category_theory.sites.surjective
category_theory.adjunction.evaluation

# Unneeded in category_theory.subobject.mono_over
category_theory.functor.currying

# Unneeded in combinatorics.pigeonhole
data.nat.modeq

# Unneeded in combinatorics.quiver.path
algebra.group.defs

# Unneeded in combinatorics.set_family.compression.down
data.fintype.basic

# Unneeded in combinatorics.set_family.harris_kleitman
algebra.big_operators.basic

# Unneeded in combinatorics.simple_graph.adj_matrix
data.rel

# Unneeded in combinatorics.simple_graph.coloring
combinatorics.simple_graph.subgraph
order.antichain

# Unneeded in combinatorics.simple_graph.connectivity
data.list.default

# Unneeded in computability.NFA
data.set.functor

# Unneeded in computability.primrec
data.list.join

# Unneeded in control.fix
data.stream.init

# Unneeded in control.functor.multivariate
logic.function.basic

# Unneeded in control.random
control.monad.basic

# Unneeded in control.traversable.derive
control.traversable.lemmas

# Unneeded in control.traversable.equiv
control.traversable.lemmas

# Unneeded in data.countable.small
data.countable.basic

# Unneeded in data.dfinsupp.basic
algebra.module.pi

# Unneeded in data.fin.vec_notation
data.fin.tuple.default

# Unneeded in data.finite.card
data.finite.basic

# Unneeded in data.finite.set
data.finite.basic
data.set.finite

# Unneeded in data.finset.fin
data.finset.card

# Unneeded in data.finset.sum
data.finset.card

# Unneeded in data.finsupp.defs
algebra.hom.group_action

# Unneeded in data.finsupp.fin
data.fin.tuple.default

# Unneeded in data.finsupp.lex
data.finsupp.ne_locus

# Unneeded in data.fintype.basic
data.finset.fin

# Unneeded in data.fintype.card_embedding
logic.equiv.fin

# Unneeded in data.fintype.order
order.conditionally_complete_lattice

# Unneeded in data.int.basic
order.monotone

# Unneeded in data.int.cast.field
data.nat.cast.field

# Unneeded in data.int.char_zero
algebra.char_zero

# Unneeded in data.int.modeq
algebra.euclidean_domain.basic

# Unneeded in data.list.big_operators
algebra.group_power.default

# Unneeded in data.list.defs
data.option.defs
data.rbtree.default_lt

# Unneeded in data.list.min_max
algebra.order.monoid.with_top

# Unneeded in data.list.pairwise
data.set.pairwise

# Unneeded in data.list.zip
algebra.order.group.min_max

# Unneeded in data.multiset.antidiagonal
data.multiset.bind

# Unneeded in data.multiset.basic
data.bool.all_any

# Unneeded in data.multiset.fintype
algebra.big_operators.default
data.fintype.card

# Unneeded in data.mv_polynomial.equiv
data.polynomial.lifts

# Unneeded in data.nat.basic
algebra.ring.basic

# Unneeded in data.nat.cast.basic
algebra.group.prod

# Unneeded in data.nat.cast.with_top
data.nat.cast.basic

# Unneeded in data.nat.choose.central
data.nat.choose.sum

# Unneeded in data.nat.count
data.list.basic
data.nat.prime
set_theory.cardinal.finite

# Unneeded in data.nat.digits
data.nat.parity

# Unneeded in data.nat.multiplicity
ring_theory.int.basic

# Unneeded in data.nat.pairing
algebra.order.group.min_max
algebra.order.monoid.prod

# Unneeded in data.nat.part_enat
order.well_founded

# Unneeded in data.nat.prime
data.nat.sqrt_norm_num

# Unneeded in data.option.basic
logic.relator

# Unneeded in data.part
data.set.basic

# Unneeded in data.pi.algebra
data.prod.basic

# Unneeded in data.pi.lex
order.min_max

# Unneeded in data.polynomial.degree.definitions
data.polynomial.induction

# Unneeded in data.polynomial.eval
algebra.geom_sum

# Unneeded in data.polynomial.hasse_deriv
data.polynomial.degree.lemmas

# Unneeded in data.polynomial.induction
data.polynomial.coeff

# Unneeded in data.polynomial.monic
algebra.associated

# Unneeded in data.rat.encodable
data.rat.defs

# Unneeded in data.rbmap.default
data.rbtree.default

# Unneeded in data.real.irrational
data.polynomial.eval

# Unneeded in data.rel
order.galois_connection

# Unneeded in data.seq.computation
logic.relator

# Unneeded in data.set.enumerate
data.set.lattice

# Unneeded in data.set.intervals.basic
order.rel_iso.basic

# Unneeded in data.set.intervals.instances
data.set.intervals.proj_Icc

# Unneeded in data.set.intervals.proj_Icc
data.set.function

# Unneeded in data.set.lattice
data.nat.basic
order.galois_connection

# Unneeded in data.set.mul_antidiagonal
data.set.pointwise.basic

# Unneeded in data.sum.basic
data.option.basic

# Unneeded in data.sym.basic
data.vector.basic

# Unneeded in data.zmod.defs
data.int.modeq

# Unneeded in deprecated.subfield
algebra.group_with_zero.power

# Unneeded in dynamics.fixed_points.topology
dynamics.fixed_points.basic

# Unneeded in dynamics.minimal
topology.algebra.mul_action

# Unneeded in dynamics.periodic_pts
data.set.pointwise.basic

# Unneeded in field_theory.finite.basic
algebra.ring.equiv
data.zmod.algebra
linear_algebra.finite_dimensional

# Unneeded in field_theory.finite.trace
field_theory.finite.basic

# Unneeded in field_theory.galois
ring_theory.power_basis

# Unneeded in field_theory.is_alg_closed.classification
data.W.cardinal
field_theory.intermediate_field

# Unneeded in field_theory.laurent
ring_theory.laurent_series

# Unneeded in field_theory.perfect_closure
algebra.group_with_zero.power

# Unneeded in field_theory.primitive_element
field_theory.fixed

# Unneeded in field_theory.separable
algebra.polynomial.big_operators

# Unneeded in geometry.euclidean.angle.oriented.basic
analysis.complex.arg

# Unneeded in geometry.euclidean.inversion
geometry.euclidean.basic

# Unneeded in geometry.manifold.instances.real
linear_algebra.finite_dimensional

# Unneeded in geometry.manifold.instances.sphere
geometry.manifold.instances.real

# Unneeded in geometry.manifold.whitney_embedding
geometry.manifold.instances.real

# Unneeded in group_theory.commensurable
group_theory.quotient_group

# Unneeded in group_theory.divisible
group_theory.group_action.pi

# Unneeded in group_theory.exponent
algebra.punit_instances

# Unneeded in group_theory.finiteness
data.finset.default

# Unneeded in group_theory.free_product
group_theory.subgroup.pointwise

# Unneeded in group_theory.group_action.basic
algebra.hom.group_action
data.fintype.card

# Unneeded in group_theory.group_action.opposite
algebra.group_with_zero.basic

# Unneeded in group_theory.group_action.quotient
group_theory.quotient_group

# Unneeded in group_theory.order_of_element
data.int.order.units

# Unneeded in group_theory.perm.basic
data.nat.cast.prod

# Unneeded in group_theory.specific_groups.dihedral
data.fintype.card
data.int.parity

# Unneeded in group_theory.submonoid.operations
algebra.order.group.defs

# Unneeded in group_theory.subsemigroup.membership
group_theory.subsemigroup.operations

# Unneeded in group_theory.torsion
algebra.is_prime_pow
group_theory.p_group

# Unneeded in linear_algebra.adic_completion
ring_theory.ideal.quotient

# Unneeded in linear_algebra.affine_space.affine_map
linear_algebra.affine_space.basic

# Unneeded in linear_algebra.affine_space.affine_subspace
data.set.intervals.unordered_interval

# Unneeded in linear_algebra.affine_space.ordered
linear_algebra.affine_space.midpoint

# Unneeded in linear_algebra.affine_space.slope
algebra.order.module

# Unneeded in linear_algebra.alternating
logic.equiv.fin

# Unneeded in linear_algebra.annihilating_polynomial
data.set.basic
ring_theory.polynomial_algebra

# Unneeded in linear_algebra.basic
order.compactly_generated

# Unneeded in linear_algebra.bilinear_form
linear_algebra.matrix.to_lin
linear_algebra.tensor_product

# Unneeded in linear_algebra.clifford_algebra.contraction
linear_algebra.clifford_algebra.grading

# Unneeded in linear_algebra.contraction
linear_algebra.free_module.finite.rank
linear_algebra.tensor_product_basis

# Unneeded in linear_algebra.determinant
linear_algebra.multilinear.basis
ring_theory.algebra_tower

# Unneeded in linear_algebra.direct_sum.finsupp
data.finsupp.to_dfinsupp

# Unneeded in linear_algebra.dual
linear_algebra.free_module.finite.rank

# Unneeded in linear_algebra.eigenspace
linear_algebra.charpoly.basic
linear_algebra.finsupp
linear_algebra.matrix.to_lin

# Unneeded in linear_algebra.exterior_algebra.basic
algebra.ring_quot
group_theory.perm.sign

# Unneeded in linear_algebra.lagrange
logic.lemmas

# Unneeded in linear_algebra.matrix.adjugate
algebra.associated

# Unneeded in linear_algebra.matrix.charpoly.basic
ring_theory.matrix_algebra

# Unneeded in linear_algebra.matrix.hermitian
analysis.inner_product_space.spectrum

# Unneeded in linear_algebra.matrix.is_diag
linear_algebra.matrix.orthogonal

# Unneeded in linear_algebra.matrix.nonsingular_inverse
algebra.regular.smul
linear_algebra.matrix.polynomial

# Unneeded in linear_algebra.matrix.polynomial
data.polynomial.eval
data.polynomial.monic

# Unneeded in linear_algebra.matrix.schur_complement
linear_algebra.matrix.symmetric

# Unneeded in linear_algebra.matrix.transvection
linear_algebra.matrix.trace

# Unneeded in linear_algebra.multilinear.basic
data.fin.tuple.default

# Unneeded in linear_algebra.projective_space.subspace
linear_algebra.projective_space.independence

# Unneeded in linear_algebra.sesquilinear_form
linear_algebra.linear_pmap
linear_algebra.matrix.basis

# Unneeded in linear_algebra.symplectic_group
data.real.basic

# Unneeded in linear_algebra.tensor_power
algebra.direct_sum.algebra

# Unneeded in linear_algebra.vandermonde
group_theory.perm.fin

# Unneeded in logic.encodable.lattice
data.finset.basic
data.set.pairwise

# Unneeded in logic.equiv.nat
data.pnat.defs

# Unneeded in logic.equiv.option
control.equiv_functor
logic.equiv.basic

# Unneeded in logic.equiv.transfer_instance
algebra.group.type_tags

# Unneeded in logic.pairwise
logic.relation

# Unneeded in measure_theory.covering.differentiation
measure_theory.decomposition.radon_nikodym
measure_theory.function.locally_integrable

# Unneeded in measure_theory.function.conditional_expectation.basic
measure_theory.function.uniform_integrable

# Unneeded in measure_theory.function.continuous_map_dense
measure_theory.function.l1_space

# Unneeded in measure_theory.function.egorov
measure_theory.integral.set_integral

# Unneeded in measure_theory.function.jacobian
measure_theory.covering.differentiation

# Unneeded in measure_theory.function.simple_func_dense
measure_theory.integral.mean_inequalities
topology.continuous_function.compact
topology.metric_space.metrizable

# Unneeded in measure_theory.function.special_functions.arctan
measure_theory.function.special_functions.basic

# Unneeded in measure_theory.function.special_functions.inner
measure_theory.function.special_functions.basic

# Unneeded in measure_theory.function.strongly_measurable.basic
measure_theory.function.ess_sup
measure_theory.integral.mean_inequalities
topology.continuous_function.compact

# Unneeded in measure_theory.function.strongly_measurable.inner
measure_theory.function.special_functions.inner

# Unneeded in measure_theory.group.fundamental_domain
measure_theory.group.pointwise

# Unneeded in measure_theory.integral.bochner
analysis.normed_space.bounded_linear_maps
topology.sequences

# Unneeded in measure_theory.integral.circle_transform
analysis.analytic.basic
analysis.calculus.parametric_interval_integral
analysis.complex.cauchy_integral

# Unneeded in measure_theory.integral.divergence_theorem
data.set.intervals.monotone

# Unneeded in measure_theory.integral.exp_decay
analysis.special_functions.exponential
analysis.special_functions.integrals

# Unneeded in measure_theory.integral.interval_average
analysis.convex.integral

# Unneeded in measure_theory.integral.interval_integral
analysis.calculus.extend_deriv

# Unneeded in measure_theory.integral.lebesgue
measure_theory.measure.mutually_singular

# Unneeded in measure_theory.measurable_space
algebra.indicator_function
measure_theory.tactic
order.filter.lift

# Unneeded in measure_theory.measurable_space_def
order.symm_diff

# Unneeded in measure_theory.measure.doubling
measure_theory.measure.measure_space

# Unneeded in measure_theory.measure.finite_measure
measure_theory.integral.set_integral

# Unneeded in measure_theory.measure.haar_quotient
topology.compact_open

# Unneeded in measure_theory.measure.hausdorff
logic.equiv.list

# Unneeded in measure_theory.measure.measure_space_def
data.set.accumulate

# Unneeded in measure_theory.tactic
measure_theory.measure.measure_space_def

# Unneeded in model_theory.basic
category_theory.concrete_category.bundled
data.fin.tuple.basic
logic.encodable.basic
logic.small.list

# Unneeded in model_theory.definability
logic.equiv.fintype

# Unneeded in model_theory.graph
model_theory.satisfiability

# Unneeded in model_theory.syntax
data.list.prod_sigma

# Unneeded in number_theory.class_number.admissible_absolute_value
data.fin.tuple.default

# Unneeded in number_theory.function_field
ring_theory.algebraic

# Unneeded in number_theory.legendre_symbol.add_character
field_theory.finite.galois_field

# Unneeded in number_theory.legendre_symbol.jacobi_symbol
data.zmod.coprime

# Unneeded in number_theory.legendre_symbol.mul_character
ring_theory.integral_domain

# Unneeded in number_theory.lucas_primality
data.zmod.basic

# Unneeded in number_theory.modular
analysis.matrix

# Unneeded in number_theory.multiplicity
number_theory.padics.padic_norm

# Unneeded in number_theory.padics.padic_integers
data.int.modeq

# Unneeded in number_theory.padics.padic_numbers
analysis.normed_space.basic

# Unneeded in number_theory.padics.padic_val
algebra.order.absolute_value

# Unneeded in number_theory.prime_counting
algebra.periodic

# Unneeded in number_theory.pythagorean_triples
algebra.group_with_zero.power

# Unneeded in number_theory.ramification_inertia
algebra.is_prime_pow
field_theory.separable
linear_algebra.free_module.pid
linear_algebra.matrix.nonsingular_inverse
ring_theory.localization.module

# Unneeded in order.bounded
order.min_max

# Unneeded in order.category.omega_complete_partial_order
order.category.Preorder

# Unneeded in order.compactly_generated
data.finite.default

# Unneeded in order.extension.linear
data.set.lattice

# Unneeded in order.filter.zero_and_bounded_at_filter
order.filter.default

# Unneeded in order.game_add
order.basic

# Unneeded in order.grade
data.nat.interval
order.atoms

# Unneeded in order.iterate
data.nat.basic

# Unneeded in order.ord_continuous
logic.function.iterate

# Unneeded in order.partial_sups
data.set.pairwise

# Unneeded in order.partition.finpartition
order.locally_finite

# Unneeded in order.rel_iso.set
logic.equiv.set

# Unneeded in order.semiconj_Sup
algebra.hom.equiv.basic

# Unneeded in order.succ_pred.linear_locally_finite
data.set.countable

# Unneeded in order.sup_indep
data.set.finite

# Unneeded in probability.conditional_expectation
probability.notation

# Unneeded in probability.conditional_probability
probability.independence

# Unneeded in probability.independence
algebra.big_operators.intervals

# Unneeded in probability.martingale.basic
probability.notation
probability.process.hitting_time

# Unneeded in probability.martingale.borel_cantelli
probability.conditional_expectation

# Unneeded in probability.notation
measure_theory.function.conditional_expectation.real

# Unneeded in probability.strong_law
measure_theory.function.l2_space

# Unneeded in probability.variance
probability.notation

# Unneeded in representation_theory.basic
linear_algebra.free_module.basic
linear_algebra.trace

# Unneeded in representation_theory.group_cohomology_resolution
algebra.homology.quasi_iso

# Unneeded in representation_theory.maschke
algebra.regular.basic

# Unneeded in ring_theory.adjoin.tower
ring_theory.algebra_tower

# Unneeded in ring_theory.adjoin_root
linear_algebra.finite_dimensional

# Unneeded in ring_theory.chain_of_divisors
algebra.is_prime_pow

# Unneeded in ring_theory.discrete_valuation_ring
order.conditionally_complete_lattice

# Unneeded in ring_theory.etale
linear_algebra.isomorphisms

# Unneeded in ring_theory.euclidean_domain
ring_theory.coprime.basic

# Unneeded in ring_theory.filtration
order.hom.complete_lattice

# Unneeded in ring_theory.finite_type
ring_theory.ideal.quotient
ring_theory.mv_polynomial.tower

# Unneeded in ring_theory.graded_algebra.basic
group_theory.subgroup.basic

# Unneeded in ring_theory.hahn_series
algebra.module.pi

# Unneeded in ring_theory.ideal.basic
order.zorn

# Unneeded in ring_theory.ideal.cotangent
ring_theory.nakayama

# Unneeded in ring_theory.ideal.minimal_prime
ring_theory.localization.integral

# Unneeded in ring_theory.ideal.norm
linear_algebra.isomorphisms
ring_theory.dedekind_domain.ideal

# Unneeded in ring_theory.integral_domain
data.fintype.card

# Unneeded in ring_theory.is_tensor_product
logic.equiv.transfer_instance

# Unneeded in ring_theory.local_properties
group_theory.submonoid.pointwise
logic.equiv.transfer_instance

# Unneeded in ring_theory.localization.integral
algebra.ring.equiv
group_theory.submonoid.inverses
ring_theory.ideal.quotient

# Unneeded in ring_theory.mv_polynomial.homogeneous
algebra.direct_sum.internal
data.fintype.card

# Unneeded in ring_theory.mv_polynomial.symmetric
data.fintype.card

# Unneeded in ring_theory.noetherian
algebra.algebra.subalgebra.tower
data.multiset.finset_ops

# Unneeded in ring_theory.non_unital_subsemiring.basic
algebra.module.basic
group_theory.submonoid.centralizer

# Unneeded in ring_theory.ore_localization.basic
algebra.group_with_zero.basic
group_theory.congruence

# Unneeded in ring_theory.ore_localization.ore_set
group_theory.subgroup.basic

# Unneeded in ring_theory.polynomial.dickson
field_theory.finite.basic

# Unneeded in ring_theory.polynomial.opposites
data.polynomial.induction

# Unneeded in ring_theory.power_series.basic
algebra.big_operators.nat_antidiagonal

# Unneeded in ring_theory.rees_algebra
ring_theory.ideal.local_ring
ring_theory.nakayama

# Unneeded in ring_theory.ring_hom.finite
ring_theory.local_properties

# Unneeded in ring_theory.ring_hom.integral
ring_theory.localization.integral
ring_theory.local_properties

# Unneeded in ring_theory.subring.pointwise
group_theory.subgroup.pointwise
ring_theory.subsemiring.pointwise

# Unneeded in ring_theory.subsemiring.pointwise
group_theory.submonoid.pointwise

# Unneeded in ring_theory.tensor_product
linear_algebra.tensor_product_basis

# Unneeded in ring_theory.valuation.basic
algebra.punit_instances

# Unneeded in ring_theory.valuation.tfae
ring_theory.valuation.valuation_subring

# Unneeded in ring_theory.witt_vector.structure_polynomial
data.fin.vec_notation

# Unneeded in set_theory.cardinal.ordinal
set_theory.ordinal.principal

# Unneeded in set_theory.game.short
set_theory.game.basic

# Unneeded in set_theory.surreal.dyadic
ring_theory.localization.away

# Unneeded in tactic.cancel_denoms
meta.expr

# Unneeded in tactic.choose
logic.function.basic

# Unneeded in tactic.clear
data.bool.basic

# Unneeded in tactic.compute_degree
data.polynomial.degree.lemmas

# Unneeded in tactic.converter.binders
order.complete_lattice

# Unneeded in tactic.elementwise
category_theory.concrete_category.basic

# Unneeded in tactic.equiv_rw
control.equiv_functor.instances
logic.equiv.defs
logic.equiv.functor

# Unneeded in tactic.ext
logic.function.basic

# Unneeded in tactic.fin_cases
data.fintype.basic

# Unneeded in tactic.find_unused
data.bool.basic

# Unneeded in tactic.group
algebra.group.commutator

# Unneeded in tactic.interactive
logic.nonempty

# Unneeded in tactic.interval_cases
data.fin.interval
data.int.interval
data.pnat.basic
data.pnat.interval

# Unneeded in tactic.lint.misc
data.bool.basic

# Unneeded in tactic.lint.type_classes
data.bool.basic

# Unneeded in tactic.monotonicity.interactive
control.traversable.derive
control.traversable.lemmas

# Unneeded in tactic.move_add
algebra.group.basic

# Unneeded in tactic.nontriviality
logic.nontrivial

# Unneeded in tactic.norm_swap
logic.equiv.defs

# Unneeded in tactic.pi_instances
order.basic

# Unneeded in tactic.positivity
algebra.order.field.power

# Unneeded in tactic.qify
data.rat.cast

# Unneeded in tactic.reassoc_axiom
category_theory.category.basic

# Unneeded in tactic.slice
category_theory.category.basic

# Unneeded in tactic.slim_check
data.list.sort

# Unneeded in tactic.suggest
data.bool.basic

# Unneeded in tactic.tfae
data.list.tfae

# Unneeded in tactic.transfer
logic.relator

# Unneeded in tactic.trunc_cases
data.quot

# Unneeded in tactic.zify
data.int.cast.lemmas
data.int.char_zero

# Unneeded in topology.algebra.algebra
topology.algebra.field

# Unneeded in topology.algebra.const_mul_action
data.real.nnreal

# Unneeded in topology.algebra.group_completion
algebra.hom.group_instances

# Unneeded in topology.algebra.mul_action
group_theory.group_action.basic

# Unneeded in topology.algebra.nonarchimedean.adic_topology
topology.algebra.uniform_ring

# Unneeded in topology.algebra.open_subgroup
topology.algebra.filter_basis

# Unneeded in topology.algebra.polynomial
analysis.normed_space.basic

# Unneeded in topology.algebra.star
topology.algebra.group

# Unneeded in topology.algebra.uniform_mul_action
algebra.hom.group_instances

# Unneeded in topology.basic
order.filter.small_sets

# Unneeded in topology.category.CompHaus.default
topology.category.Top.default

# Unneeded in topology.category.Profinite.default
category_theory.limits.constructions.epi_mono

# Unneeded in topology.category.Top.epi_mono
category_theory.epi_mono

# Unneeded in topology.category.Top.limits
category_theory.limits.preserves.limits
category_theory.limits.shapes.types

# Unneeded in topology.category.UniformSpace
category_theory.limits.has_limits
category_theory.monad.limits

# Unneeded in topology.connected
data.int.succ_pred
data.nat.succ_pred
order.partial_sups

# Unneeded in topology.constructions
data.fin.tuple.default

# Unneeded in topology.continuous_function.polynomial
topology.continuous_function.compact

# Unneeded in topology.continuous_function.stone_weierstrass
analysis.complex.basic

# Unneeded in topology.continuous_function.units
topology.continuous_function.compact

# Unneeded in topology.gluing
topology.category.Top.default

# Unneeded in topology.instances.matrix
linear_algebra.determinant

# Unneeded in topology.instances.real
order.filter.archimedean

# Unneeded in topology.instances.real_vector_space
topology.instances.real

# Unneeded in topology.locally_constant.basic
topology.algebra.monoid

# Unneeded in topology.metric_space.basic
data.int.interval
topology.uniform_space.complete_separated

# Unneeded in topology.metric_space.cau_seq_filter
analysis.normed_space.basic

# Unneeded in topology.metric_space.polish
analysis.normed_space.basic

# Unneeded in topology.noetherian_space
order.order_iso_nat

# Unneeded in topology.order
topology.tactic

# Unneeded in topology.order.hom.esakia
order.hom.order

# Unneeded in topology.semicontinuous
topology.algebra.group

# Unneeded in topology.sheaves.limits
category_theory.adjunction.default

# Unneeded in topology.sheaves.operations
algebra.category.Group.limits
category_theory.sites.compatible_sheafification
topology.sheaves.sheafify

# Unneeded in topology.sheaves.presheaf
category_theory.adjunction.default

# Unneeded in topology.sheaves.sheaf
category_theory.full_subcategory
category_theory.limits.unit

# Unneeded in topology.sheaves.sheaf_of_functions
category_theory.limits.shapes.types

# Unneeded in topology.sheaves.skyscraper
algebraic_geometry.sheafed_space
category_theory.preadditive.injective

# Unneeded in topology.sheaves.stalks
algebra.category.Ring.default
topology.sober

# Unneeded in topology.sober
topology.continuous_function.basic

# Unneeded in topology.uniform_space.separation
data.set.pairwise