Commit 2024-04-09 06:29 aee79f61

View on Github →

refactor(LinearAlgebra/BilinForm): Remove structure BilinForm from Mathlib, migrate all of _root_.BilinForm to LinearMap.BilinForm (#11278) Remove structure BilinForm from LinearAlgebra/BilinearForm/Basic and migrate all of _root_.BilinForm to LinearMap.BilinForm Closes: #10553 This isn't the end of the story, as there's still a lot of overlap between LinearAlgebra/BilinearForm and LinearAlgebra/SesquilinearForm but that can be sorted out in subsequent PRs. Supersedes:

Estimated changes

Modified Mathlib/LinearAlgebra/BilinearForm/Basic.lean

deleted theorem BilinForm.add_apply

deleted theorem BilinForm.add_left

deleted theorem BilinForm.add_right

deleted def BilinForm.coeFnAddMonoidHom

deleted theorem BilinForm.coeFn_congr

deleted theorem BilinForm.coeFn_mk

deleted theorem BilinForm.coe_add

deleted theorem BilinForm.coe_injective

deleted theorem BilinForm.coe_neg

deleted theorem BilinForm.coe_smul

deleted theorem BilinForm.coe_sub

deleted theorem BilinForm.coe_zero

deleted theorem BilinForm.congr_fun

deleted theorem BilinForm.ext

deleted theorem BilinForm.ext_iff

deleted def BilinForm.flipHom

deleted def BilinForm.flipHomAux

deleted theorem BilinForm.flip_apply

deleted theorem BilinForm.flip_flip

deleted theorem BilinForm.flip_flip_aux

deleted theorem BilinForm.neg_apply

deleted theorem BilinForm.neg_left

deleted theorem BilinForm.neg_right

deleted def BilinForm.restrict

deleted theorem BilinForm.smul_apply

deleted theorem BilinForm.smul_left

deleted theorem BilinForm.smul_left_of_tower

deleted theorem BilinForm.smul_right

deleted theorem BilinForm.smul_right_of_tower

deleted theorem BilinForm.sub_apply

deleted theorem BilinForm.sub_left

deleted theorem BilinForm.sub_right

deleted theorem BilinForm.zero_apply

deleted theorem BilinForm.zero_left

deleted theorem BilinForm.zero_right

deleted structure BilinForm

added theorem LinearMap.BilinForm.add_apply

added theorem LinearMap.BilinForm.add_left

added theorem LinearMap.BilinForm.add_right

added def LinearMap.BilinForm.coeFnAddMonoidHom

added theorem LinearMap.BilinForm.coeFn_congr

added theorem LinearMap.BilinForm.coe_add

added theorem LinearMap.BilinForm.coe_injective

added theorem LinearMap.BilinForm.coe_neg

added theorem LinearMap.BilinForm.coe_sub

added theorem LinearMap.BilinForm.coe_zero

added theorem LinearMap.BilinForm.congr_fun

added theorem LinearMap.BilinForm.ext

added theorem LinearMap.BilinForm.ext_iff

added def LinearMap.BilinForm.flipHom

added def LinearMap.BilinForm.flipHomAux

added theorem LinearMap.BilinForm.flip_apply

added theorem LinearMap.BilinForm.flip_flip

added theorem LinearMap.BilinForm.flip_flip_aux

added theorem LinearMap.BilinForm.neg_apply

added theorem LinearMap.BilinForm.neg_left

added theorem LinearMap.BilinForm.neg_right

added def LinearMap.BilinForm.restrict

added theorem LinearMap.BilinForm.smul_left

added theorem LinearMap.BilinForm.smul_left_of_tower

added theorem LinearMap.BilinForm.smul_right

added theorem LinearMap.BilinForm.smul_right_of_tower

added theorem LinearMap.BilinForm.sub_apply

added theorem LinearMap.BilinForm.sub_left

added theorem LinearMap.BilinForm.sub_right

added theorem LinearMap.BilinForm.zero_apply

added theorem LinearMap.BilinForm.zero_left

added theorem LinearMap.BilinForm.zero_right

Modified Mathlib/LinearAlgebra/BilinearForm/DualLattice.lean

deleted def BilinForm.dualSubmodule

deleted def BilinForm.dualSubmoduleParing

deleted theorem BilinForm.dualSubmoduleParing_spec

deleted def BilinForm.dualSubmoduleToDual

deleted theorem BilinForm.dualSubmoduleToDual_injective

deleted theorem BilinForm.dualSubmodule_dualSubmodule_flip_of_basis

deleted theorem BilinForm.dualSubmodule_dualSubmodule_of_basis

deleted theorem BilinForm.dualSubmodule_flip_dualSubmodule_of_basis

deleted theorem BilinForm.dualSubmodule_span_of_basis

deleted theorem BilinForm.le_flip_dualSubmodule

deleted theorem BilinForm.mem_dualSubmodule

added def LinearMap.BilinForm.dualSubmodule

added def LinearMap.BilinForm.dualSubmoduleParing

added theorem LinearMap.BilinForm.dualSubmoduleParing_spec

added def LinearMap.BilinForm.dualSubmoduleToDual

added theorem LinearMap.BilinForm.dualSubmoduleToDual_injective

added theorem LinearMap.BilinForm.dualSubmodule_dualSubmodule_flip_of_basis

added theorem LinearMap.BilinForm.dualSubmodule_dualSubmodule_of_basis

added theorem LinearMap.BilinForm.dualSubmodule_flip_dualSubmodule_of_basis

added theorem LinearMap.BilinForm.dualSubmodule_span_of_basis

added theorem LinearMap.BilinForm.le_flip_dualSubmodule

added theorem LinearMap.BilinForm.mem_dualSubmodule

Modified Mathlib/LinearAlgebra/BilinearForm/Hom.lean

deleted def BilinForm.comp

deleted def BilinForm.compLeft

deleted theorem BilinForm.compLeft_apply

deleted theorem BilinForm.compLeft_compRight

deleted theorem BilinForm.compLeft_id

deleted def BilinForm.compRight

deleted theorem BilinForm.compRight_apply

deleted theorem BilinForm.compRight_compLeft

deleted theorem BilinForm.compRight_id

deleted theorem BilinForm.comp_apply

deleted theorem BilinForm.comp_comp

deleted theorem BilinForm.comp_congr

deleted theorem BilinForm.comp_id_id

deleted theorem BilinForm.comp_id_left

deleted theorem BilinForm.comp_id_right

deleted theorem BilinForm.comp_inj

deleted def BilinForm.congr

deleted theorem BilinForm.congr_apply

deleted theorem BilinForm.congr_comp

deleted theorem BilinForm.congr_congr

deleted theorem BilinForm.congr_refl

deleted theorem BilinForm.congr_symm

deleted theorem BilinForm.congr_trans

deleted theorem BilinForm.ext_basis

deleted def BilinForm.linMulLin

deleted theorem BilinForm.linMulLin_apply

deleted theorem BilinForm.linMulLin_comp

deleted theorem BilinForm.linMulLin_compLeft

deleted theorem BilinForm.linMulLin_compRight

deleted theorem BilinForm.sum_apply

deleted theorem BilinForm.sum_left

deleted theorem BilinForm.sum_repr_mul_repr_mul

deleted theorem BilinForm.sum_right

deleted theorem BilinForm.toLin'Flip_apply

deleted theorem BilinForm.toLin'_apply

deleted def BilinForm.toLin

deleted def BilinForm.toLinHom

deleted def BilinForm.toLinHomAux₁

deleted def BilinForm.toLinHomAux₂

deleted def BilinForm.toLinHomFlip

modified theorem BilinForm.toLin_apply

added def LinearMap.BilinForm.comp

added def LinearMap.BilinForm.compLeft

added theorem LinearMap.BilinForm.compLeft_apply

added theorem LinearMap.BilinForm.compLeft_compRight

added theorem LinearMap.BilinForm.compLeft_id

added def LinearMap.BilinForm.compRight

added theorem LinearMap.BilinForm.compRight_apply

added theorem LinearMap.BilinForm.compRight_compLeft

added theorem LinearMap.BilinForm.compRight_id

added theorem LinearMap.BilinForm.comp_apply

added theorem LinearMap.BilinForm.comp_comp

added theorem LinearMap.BilinForm.comp_congr

added theorem LinearMap.BilinForm.comp_id_id

added theorem LinearMap.BilinForm.comp_id_left

added theorem LinearMap.BilinForm.comp_id_right

added theorem LinearMap.BilinForm.comp_inj

added def LinearMap.BilinForm.congr

added theorem LinearMap.BilinForm.congr_apply

added theorem LinearMap.BilinForm.congr_comp

added theorem LinearMap.BilinForm.congr_congr

added theorem LinearMap.BilinForm.congr_refl

added theorem LinearMap.BilinForm.congr_symm

added theorem LinearMap.BilinForm.congr_trans

added theorem LinearMap.BilinForm.ext_basis

added def LinearMap.BilinForm.linMulLin

added theorem LinearMap.BilinForm.linMulLin_apply

added theorem LinearMap.BilinForm.linMulLin_comp

added theorem LinearMap.BilinForm.linMulLin_compLeft

added theorem LinearMap.BilinForm.linMulLin_compRight

added theorem LinearMap.BilinForm.sum_apply

added theorem LinearMap.BilinForm.sum_left

added theorem LinearMap.BilinForm.sum_repr_mul_repr_mul

added theorem LinearMap.BilinForm.sum_right

added theorem LinearMap.BilinForm.toLin'Flip_apply

added theorem LinearMap.BilinForm.toLin'_apply

added def LinearMap.BilinForm.toLin

added def LinearMap.BilinForm.toLinHom

added def LinearMap.BilinForm.toLinHomAux₁

added def LinearMap.BilinForm.toLinHomAux₂

added def LinearMap.BilinForm.toLinHomFlip

modified def LinearMap.compBilinForm

modified def LinearMap.toBilinAux

Modified Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean

deleted theorem BilinForm.IsAlt.ortho_comm

deleted def BilinForm.IsOrtho

deleted theorem BilinForm.IsRefl.ortho_comm

deleted theorem BilinForm.IsSymm.ortho_comm

deleted theorem BilinForm.finrank_add_finrank_orthogonal

deleted theorem BilinForm.iIsOrtho.nondegenerate_iff_not_isOrtho_basis_self

deleted theorem BilinForm.iIsOrtho.not_isOrtho_basis_self_of_nondegenerate

deleted def BilinForm.iIsOrtho

deleted theorem BilinForm.iIsOrtho_def

deleted theorem BilinForm.isCompl_span_singleton_orthogonal

deleted theorem BilinForm.isOrtho_def

deleted theorem BilinForm.isOrtho_smul_left

deleted theorem BilinForm.isOrtho_smul_right

deleted theorem BilinForm.isOrtho_zero_left

deleted theorem BilinForm.isOrtho_zero_right

deleted theorem BilinForm.le_orthogonal_orthogonal

deleted theorem BilinForm.linearIndependent_of_iIsOrtho

deleted theorem BilinForm.mem_orthogonal_iff

deleted theorem BilinForm.ne_zero_of_not_isOrtho_self

deleted theorem BilinForm.nondegenerateRestrictOfDisjointOrthogonal

deleted def BilinForm.orthogonal

deleted theorem BilinForm.orthogonal_le

deleted theorem BilinForm.orthogonal_span_singleton_eq_toLin_ker

deleted theorem BilinForm.restrictOrthogonalSpanSingletonNondegenerate

deleted theorem BilinForm.restrict_nondegenerate_iff_isCompl_orthogonal

deleted theorem BilinForm.restrict_nondegenerate_of_isCompl_orthogonal

deleted theorem BilinForm.span_singleton_inf_orthogonal_eq_bot

deleted theorem BilinForm.span_singleton_sup_orthogonal_eq_top

deleted theorem BilinForm.toLin_restrict_ker_eq_inf_orthogonal

deleted theorem BilinForm.toLin_restrict_range_dualCoannihilator_eq_orthogonal

added theorem LinearMap.BilinForm.IsAlt.ortho_comm

added def LinearMap.BilinForm.IsOrtho

added theorem LinearMap.BilinForm.IsRefl.ortho_comm

added theorem LinearMap.BilinForm.IsSymm.ortho_comm

added theorem LinearMap.BilinForm.finrank_add_finrank_orthogonal

added theorem LinearMap.BilinForm.iIsOrtho.nondegenerate_iff_not_isOrtho_basis_self

added theorem LinearMap.BilinForm.iIsOrtho.not_isOrtho_basis_self_of_nondegenerate

added def LinearMap.BilinForm.iIsOrtho

added theorem LinearMap.BilinForm.iIsOrtho_def

added theorem LinearMap.BilinForm.isCompl_span_singleton_orthogonal

added theorem LinearMap.BilinForm.isOrtho_def

added theorem LinearMap.BilinForm.isOrtho_smul_left

added theorem LinearMap.BilinForm.isOrtho_smul_right

added theorem LinearMap.BilinForm.isOrtho_zero_left

added theorem LinearMap.BilinForm.isOrtho_zero_right

added theorem LinearMap.BilinForm.le_orthogonal_orthogonal

added theorem LinearMap.BilinForm.linearIndependent_of_iIsOrtho

added theorem LinearMap.BilinForm.mem_orthogonal_iff

added theorem LinearMap.BilinForm.ne_zero_of_not_isOrtho_self

added theorem LinearMap.BilinForm.nondegenerateRestrictOfDisjointOrthogonal

added def LinearMap.BilinForm.orthogonal

added theorem LinearMap.BilinForm.orthogonal_le

added theorem LinearMap.BilinForm.orthogonal_span_singleton_eq_toLin_ker

added theorem LinearMap.BilinForm.restrictOrthogonalSpanSingletonNondegenerate

added theorem LinearMap.BilinForm.restrict_nondegenerate_iff_isCompl_orthogonal

added theorem LinearMap.BilinForm.restrict_nondegenerate_of_isCompl_orthogonal

added theorem LinearMap.BilinForm.span_singleton_inf_orthogonal_eq_bot

added theorem LinearMap.BilinForm.span_singleton_sup_orthogonal_eq_top

added theorem LinearMap.BilinForm.toLin_restrict_ker_eq_inf_orthogonal

added theorem LinearMap.BilinForm.toLin_restrict_range_dualCoannihilator_eq_orthogonal

Modified Mathlib/LinearAlgebra/BilinearForm/Properties.lean

deleted theorem BilinForm.IsAdjointPair.add

deleted theorem BilinForm.IsAdjointPair.comp

deleted theorem BilinForm.IsAdjointPair.eq

deleted theorem BilinForm.IsAdjointPair.mul

deleted theorem BilinForm.IsAdjointPair.smul

deleted theorem BilinForm.IsAdjointPair.sub

deleted def BilinForm.IsAdjointPair

deleted theorem BilinForm.IsAlt.isRefl

deleted theorem BilinForm.IsAlt.neg_eq

deleted theorem BilinForm.IsAlt.self_eq_zero

deleted def BilinForm.IsAlt

deleted def BilinForm.IsPairSelfAdjoint

deleted theorem BilinForm.IsRefl.eq_zero

deleted def BilinForm.IsRefl

deleted def BilinForm.IsSelfAdjoint

deleted def BilinForm.IsSkewAdjoint

deleted theorem BilinForm.IsSymm.isRefl

deleted theorem BilinForm.IsSymm.restrict

deleted def BilinForm.IsSymm

deleted theorem BilinForm.Nondegenerate.congr

deleted theorem BilinForm.Nondegenerate.flip

deleted theorem BilinForm.Nondegenerate.ker_eq_bot

deleted theorem BilinForm.Nondegenerate.ne_zero

deleted def BilinForm.Nondegenerate

deleted theorem BilinForm.apply_dualBasis_left

deleted theorem BilinForm.apply_dualBasis_right

deleted theorem BilinForm.compLeft_injective

deleted theorem BilinForm.comp_symmCompOfNondegenerate_apply

deleted theorem BilinForm.dualBasis_dualBasis

deleted theorem BilinForm.dualBasis_dualBasis_flip

deleted theorem BilinForm.dualBasis_flip_dualBasis

deleted theorem BilinForm.dualBasis_repr_apply

deleted theorem BilinForm.isAdjointPairLeftAdjointOfNondegenerate

deleted theorem BilinForm.isAdjointPair_id

deleted theorem BilinForm.isAdjointPair_iff_compLeft_eq_compRight

deleted theorem BilinForm.isAdjointPair_iff_eq_of_nondegenerate

deleted theorem BilinForm.isAdjointPair_unique_of_nondegenerate

deleted theorem BilinForm.isAdjointPair_zero

deleted theorem BilinForm.isAlt_neg

deleted theorem BilinForm.isAlt_zero

deleted def BilinForm.isPairSelfAdjointSubmodule

deleted theorem BilinForm.isPairSelfAdjoint_equiv

deleted theorem BilinForm.isRefl_neg

deleted theorem BilinForm.isRefl_zero

deleted theorem BilinForm.isSkewAdjoint_iff_neg_self_adjoint

deleted theorem BilinForm.isSymm_iff_flip

deleted theorem BilinForm.isSymm_neg

deleted theorem BilinForm.isSymm_zero

deleted theorem BilinForm.mem_isPairSelfAdjointSubmodule

deleted theorem BilinForm.mem_selfAdjointSubmodule

deleted theorem BilinForm.mem_skewAdjointSubmodule

deleted theorem BilinForm.nonDegenerateFlip_iff

deleted theorem BilinForm.nondegenerate_congr_iff

deleted theorem BilinForm.nondegenerate_iff_ker_eq_bot

deleted theorem BilinForm.not_nondegenerate_zero

deleted def BilinForm.selfAdjointSubmodule

deleted def BilinForm.skewAdjointSubmodule

deleted theorem BilinForm.symmCompOfNondegenerate_left_apply

deleted theorem BilinForm.toDual_def

added theorem LinearMap.BilinForm.IsAdjointPair.add

added theorem LinearMap.BilinForm.IsAdjointPair.comp

added theorem LinearMap.BilinForm.IsAdjointPair.eq

added theorem LinearMap.BilinForm.IsAdjointPair.mul

added theorem LinearMap.BilinForm.IsAdjointPair.smul

added theorem LinearMap.BilinForm.IsAdjointPair.sub

added def LinearMap.BilinForm.IsAdjointPair

added theorem LinearMap.BilinForm.IsAlt.isRefl

added theorem LinearMap.BilinForm.IsAlt.neg_eq

added theorem LinearMap.BilinForm.IsAlt.self_eq_zero

added def LinearMap.BilinForm.IsAlt

added def LinearMap.BilinForm.IsPairSelfAdjoint

added theorem LinearMap.BilinForm.IsRefl.eq_zero

added def LinearMap.BilinForm.IsRefl

added def LinearMap.BilinForm.IsSelfAdjoint

added def LinearMap.BilinForm.IsSkewAdjoint

added theorem LinearMap.BilinForm.IsSymm.isRefl

added theorem LinearMap.BilinForm.IsSymm.restrict

added def LinearMap.BilinForm.IsSymm

added theorem LinearMap.BilinForm.Nondegenerate.congr

added theorem LinearMap.BilinForm.Nondegenerate.flip

added theorem LinearMap.BilinForm.Nondegenerate.ker_eq_bot

added theorem LinearMap.BilinForm.Nondegenerate.ne_zero

added def LinearMap.BilinForm.Nondegenerate

added theorem LinearMap.BilinForm.apply_dualBasis_left

added theorem LinearMap.BilinForm.apply_dualBasis_right

added theorem LinearMap.BilinForm.compLeft_injective

added theorem LinearMap.BilinForm.comp_symmCompOfNondegenerate_apply

added theorem LinearMap.BilinForm.dualBasis_dualBasis

added theorem LinearMap.BilinForm.dualBasis_dualBasis_flip

added theorem LinearMap.BilinForm.dualBasis_flip_dualBasis

added theorem LinearMap.BilinForm.dualBasis_repr_apply

added theorem LinearMap.BilinForm.isAdjointPairLeftAdjointOfNondegenerate

added theorem LinearMap.BilinForm.isAdjointPair_id

added theorem LinearMap.BilinForm.isAdjointPair_iff_compLeft_eq_compRight

added theorem LinearMap.BilinForm.isAdjointPair_iff_eq_of_nondegenerate

added theorem LinearMap.BilinForm.isAdjointPair_unique_of_nondegenerate

added theorem LinearMap.BilinForm.isAdjointPair_zero

added theorem LinearMap.BilinForm.isAlt_neg

added theorem LinearMap.BilinForm.isAlt_zero

added def LinearMap.BilinForm.isPairSelfAdjointSubmodule

added theorem LinearMap.BilinForm.isPairSelfAdjoint_equiv

added theorem LinearMap.BilinForm.isRefl_neg

added theorem LinearMap.BilinForm.isRefl_zero

added theorem LinearMap.BilinForm.isSkewAdjoint_iff_neg_self_adjoint

added theorem LinearMap.BilinForm.isSymm_iff_flip

added theorem LinearMap.BilinForm.isSymm_neg

added theorem LinearMap.BilinForm.isSymm_zero

added theorem LinearMap.BilinForm.mem_isPairSelfAdjointSubmodule

added theorem LinearMap.BilinForm.mem_selfAdjointSubmodule

added theorem LinearMap.BilinForm.mem_skewAdjointSubmodule

added theorem LinearMap.BilinForm.nonDegenerateFlip_iff

added theorem LinearMap.BilinForm.nondegenerate_congr_iff

added theorem LinearMap.BilinForm.nondegenerate_iff_ker_eq_bot

added theorem LinearMap.BilinForm.not_nondegenerate_zero

added def LinearMap.BilinForm.selfAdjointSubmodule

added def LinearMap.BilinForm.skewAdjointSubmodule

added theorem LinearMap.BilinForm.symmCompOfNondegenerate_left_apply

added theorem LinearMap.BilinForm.toDual_def

Modified Mathlib/LinearAlgebra/Matrix/BilinearForm.lean

deleted theorem BilinForm.Nondegenerate.toMatrix'

deleted theorem BilinForm.Nondegenerate.toMatrix

deleted theorem BilinForm.mul_toMatrix'

deleted theorem BilinForm.mul_toMatrix'_mul

deleted theorem BilinForm.nondegenerate_iff_det_ne_zero

deleted theorem BilinForm.nondegenerate_of_det_ne_zero

deleted theorem BilinForm.nondegenerate_toBilin'_iff_det_ne_zero

deleted theorem BilinForm.nondegenerate_toBilin'_of_det_ne_zero'

deleted theorem BilinForm.nondegenerate_toMatrix'_iff

deleted theorem BilinForm.nondegenerate_toMatrix_iff

deleted def BilinForm.toMatrix'

deleted theorem BilinForm.toMatrix'_apply

deleted theorem BilinForm.toMatrix'_comp

deleted theorem BilinForm.toMatrix'_compLeft

deleted theorem BilinForm.toMatrix'_compRight

deleted theorem BilinForm.toMatrix'_mul

deleted theorem BilinForm.toMatrix'_symm

deleted theorem BilinForm.toMatrix'_toBilin'

deleted theorem BilinForm.toMatrixAux_apply

deleted theorem BilinForm.toMatrixAux_stdBasis

added theorem LinearMap.BilinForm.Nondegenerate.toMatrix'

added theorem LinearMap.BilinForm.Nondegenerate.toMatrix

added theorem LinearMap.BilinForm.mul_toMatrix'

added theorem LinearMap.BilinForm.mul_toMatrix'_mul

added theorem LinearMap.BilinForm.nondegenerate_iff_det_ne_zero

added theorem LinearMap.BilinForm.nondegenerate_of_det_ne_zero

added theorem LinearMap.BilinForm.nondegenerate_toBilin'_iff_det_ne_zero

added theorem LinearMap.BilinForm.nondegenerate_toBilin'_of_det_ne_zero'

added theorem LinearMap.BilinForm.nondegenerate_toMatrix'_iff

added theorem LinearMap.BilinForm.nondegenerate_toMatrix_iff

added def LinearMap.BilinForm.toMatrix'

added theorem LinearMap.BilinForm.toMatrix'_apply

added theorem LinearMap.BilinForm.toMatrix'_comp

added theorem LinearMap.BilinForm.toMatrix'_compLeft

added theorem LinearMap.BilinForm.toMatrix'_compRight

added theorem LinearMap.BilinForm.toMatrix'_mul

added theorem LinearMap.BilinForm.toMatrix'_symm

added theorem LinearMap.BilinForm.toMatrix'_toBilin'

added theorem LinearMap.BilinForm.toMatrixAux_apply

added theorem LinearMap.BilinForm.toMatrixAux_stdBasis

Modified Mathlib/RingTheory/DedekindDomain/Different.lean

Modified Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean

Modified Mathlib/RingTheory/Discriminant.lean

Modified Mathlib/RingTheory/Trace.lean

Modified docs/overview.yaml

Modified docs/undergrad.yaml